Metamath Proof Explorer

Theorem fmptff

Description: Functionality of the mapping operation. (Contributed by Glauco Siliprandi, 5-Jan-2025)

Ref Expression
Hypotheses fmptff.1 ⊢ Ⅎ _ x A
fmptff.2 ⊢ Ⅎ _ x B
fmptff.3 ⊢ F = x ∈ A ⟼ C
Assertion fmptff ⊢ ∀ x ∈ A C ∈ B ↔ F : A ⟶ B

Proof

Step Hyp Ref Expression
1 fmptff.1 ⊢ Ⅎ _ x A
2 fmptff.2 ⊢ Ⅎ _ x B
3 fmptff.3 ⊢ F = x ∈ A ⟼ C
4 nfcv ⊢ Ⅎ _ y A
5 nfv ⊢ Ⅎ y C ∈ B
6 nfcsb1v ⊢ Ⅎ _ x ⦋ y / x⦌ C
7 6 2 nfel ⊢ Ⅎ x ⦋ y / x⦌ C ∈ B
8 csbeq1a ⊢ x = y → C = ⦋ y / x⦌ C
9 8 eleq1d ⊢ x = y → C ∈ B ↔ ⦋ y / x⦌ C ∈ B
10 1 4 5 7 9 cbvralfw ⊢ ∀ x ∈ A C ∈ B ↔ ∀ y ∈ A ⦋ y / x⦌ C ∈ B
11 nfcv ⊢ Ⅎ _ y C
12 1 4 11 6 8 cbvmptf ⊢ x ∈ A ⟼ C = y ∈ A ⟼ ⦋ y / x⦌ C
13 3 12 eqtri ⊢ F = y ∈ A ⟼ ⦋ y / x⦌ C
14 13 fmpt ⊢ ∀ y ∈ A ⦋ y / x⦌ C ∈ B ↔ F : A ⟶ B
15 10 14 bitri ⊢ ∀ x ∈ A C ∈ B ↔ F : A ⟶ B