This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fmptdF

Description: Domain and codomain of the mapping operation; deduction form. This version of fmptd uses bound-variable hypothesis instead of distinct variable conditions. (Contributed by Thierry Arnoux, 28-Mar-2017)

Ref Expression
Hypotheses fmptdF.p ⊢ Ⅎ x φ
fmptdF.a ⊢ Ⅎ _ x A
fmptdF.c ⊢ Ⅎ _ x C
fmptdF.1 ⊢ φ ∧ x ∈ A → B ∈ C
fmptdF.2 ⊢ F = x ∈ A ⟼ B
Assertion fmptdF ⊢ φ → F : A ⟶ C

Proof

Step Hyp Ref Expression
1 fmptdF.p ⊢ Ⅎ x φ
2 fmptdF.a ⊢ Ⅎ _ x A
3 fmptdF.c ⊢ Ⅎ _ x C
4 fmptdF.1 ⊢ φ ∧ x ∈ A → B ∈ C
5 fmptdF.2 ⊢ F = x ∈ A ⟼ B
6 4 sbimi ⊢ y x φ ∧ x ∈ A → y x B ∈ C
7 sban ⊢ y x φ ∧ x ∈ A ↔ y x φ ∧ y x x ∈ A
8 1 sbf ⊢ y x φ ↔ φ
9 2 clelsb1fw ⊢ y x x ∈ A ↔ y ∈ A
10 8 9 anbi12i ⊢ y x φ ∧ y x x ∈ A ↔ φ ∧ y ∈ A
11 7 10 bitri ⊢ y x φ ∧ x ∈ A ↔ φ ∧ y ∈ A
12 sbsbc ⊢ y x B ∈ C ↔ [˙y / x]˙ B ∈ C
13 sbcel12 ⊢ [˙y / x]˙ B ∈ C ↔ ⦋ y / x⦌ B ∈ ⦋ y / x⦌ C
14 vex ⊢ y ∈ V
15 14 3 csbgfi ⊢ ⦋ y / x⦌ C = C
16 15 eleq2i ⊢ ⦋ y / x⦌ B ∈ ⦋ y / x⦌ C ↔ ⦋ y / x⦌ B ∈ C
17 13 16 bitri ⊢ [˙y / x]˙ B ∈ C ↔ ⦋ y / x⦌ B ∈ C
18 12 17 bitri ⊢ y x B ∈ C ↔ ⦋ y / x⦌ B ∈ C
19 6 11 18 3imtr3i ⊢ φ ∧ y ∈ A → ⦋ y / x⦌ B ∈ C
20 19 ralrimiva ⊢ φ → ∀ y ∈ A ⦋ y / x⦌ B ∈ C
21 nfcv ⊢ Ⅎ _ y A
22 nfcv ⊢ Ⅎ _ y B
23 nfcsb1v ⊢ Ⅎ _ x ⦋ y / x⦌ B
24 csbeq1a ⊢ x = y → B = ⦋ y / x⦌ B
25 2 21 22 23 24 cbvmptf ⊢ x ∈ A ⟼ B = y ∈ A ⟼ ⦋ y / x⦌ B
26 25 fmpt ⊢ ∀ y ∈ A ⦋ y / x⦌ B ∈ C ↔ x ∈ A ⟼ B : A ⟶ C
27 20 26 sylib ⊢ φ → x ∈ A ⟼ B : A ⟶ C
28 5 feq1i ⊢ F : A ⟶ C ↔ x ∈ A ⟼ B : A ⟶ C
29 27 28 sylibr ⊢ φ → F : A ⟶ C