restr_intro

Theorem restr_intro

Theorem. restr_intro
(x, y) ∈ f → x ∈ A → (x, y) ∈ restr f A

Proof
01. 1 ⊢ (x, y) ∈ f, hypo.
02. 2 ⊢ x ∈ A, hypo.
03. 1 ⊢ set (x, y), set_intro 1.
04. 1 ⊢ set y, setr_from_pair 3.
05. 1 ⊢ y ∈ UnivCl, UnivCl_intro 4.
06. 1, 2 ⊢ (x, y) ∈ A × UnivCl, prod_intro 2 5.
07. 1, 2 ⊢ (x, y) ∈ f ∩ (A × UnivCl), intersection_intro 1 6.
08. ⊢ restr f A = f ∩ (A × UnivCl), restr_eq.
09. 1, 2 ⊢ (x, y) ∈ restr f A, eq_subst_rev 8 7, P u ↔ (x, y) ∈ u.
restr_intro. ⊢ (x, y) ∈ f → x ∈ A → (x, y) ∈ restr f A, subj_intro_ii 9.

Dependencies
The given proof depends on nine axioms:
comp, efq, eq_refl, eq_subst, ext, lem, pairing, subset, union.