Metamath Proof Explorer

Theorem fmptf

Description: Functionality of the mapping operation. (Contributed by Glauco Siliprandi, 23-Oct-2021)

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

Proof

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