Metamath Proof Explorer

Theorem abfmpeld

Description: Membership in an element of a mapping function-defined family of sets. (Contributed by Thierry Arnoux, 19-Oct-2016)

Ref Expression
Hypotheses abfmpeld.1 ⊢F=x∈V⟼y|ψ
abfmpeld.2 ⊢φ→y|ψ∈V
abfmpeld.3 ⊢φ→x=A∧y=B→ψ↔χ
Assertion abfmpeld ⊢φ→A∈V∧B∈W→B∈F⁡A↔χ

Proof

Step Hyp Ref Expression
1 abfmpeld.1 ⊢F=x∈V⟼y|ψ
2 abfmpeld.2 ⊢φ→y|ψ∈V
3 abfmpeld.3 ⊢φ→x=A∧y=B→ψ↔χ
4 2 alrimiv ⊢φ→∀xy|ψ∈V
5 csbexg ⊢∀xy|ψ∈V→⦋A/x⦌y|ψ∈V
6 4 5 syl ⊢φ→⦋A/x⦌y|ψ∈V
7 1 fvmpts ⊢A∈V∧⦋A/x⦌y|ψ∈V→F⁡A=⦋A/x⦌y|ψ
8 6 7 sylan2 ⊢A∈V∧φ→F⁡A=⦋A/x⦌y|ψ
9 csbab ⊢⦋A/x⦌y|ψ=y|[˙A/x]˙ψ
10 8 9 eqtrdi ⊢A∈V∧φ→F⁡A=y|[˙A/x]˙ψ
11 10 eleq2d ⊢A∈V∧φ→B∈F⁡A↔B∈y|[˙A/x]˙ψ
12 11 adantl ⊢B∈W∧A∈V∧φ→B∈F⁡A↔B∈y|[˙A/x]˙ψ
13 simpll ⊢A∈V∧φ∧y=B→A∈V
14 3 ancomsd ⊢φ→y=B∧x=A→ψ↔χ
15 14 adantl ⊢A∈V∧φ→y=B∧x=A→ψ↔χ
16 15 impl ⊢A∈V∧φ∧y=B∧x=A→ψ↔χ
17 13 16 sbcied ⊢A∈V∧φ∧y=B→[˙A/x]˙ψ↔χ
18 17 ex ⊢A∈V∧φ→y=B→[˙A/x]˙ψ↔χ
19 18 alrimiv ⊢A∈V∧φ→∀yy=B→[˙A/x]˙ψ↔χ
20 elabgt ⊢B∈W∧∀yy=B→[˙A/x]˙ψ↔χ→B∈y|[˙A/x]˙ψ↔χ
21 19 20 sylan2 ⊢B∈W∧A∈V∧φ→B∈y|[˙A/x]˙ψ↔χ
22 12 21 bitrd ⊢B∈W∧A∈V∧φ→B∈F⁡A↔χ
23 22 an13s ⊢φ∧A∈V∧B∈W→B∈F⁡A↔χ
24 23 ex ⊢φ→A∈V∧B∈W→B∈F⁡A↔χ