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 φ x y | ψ V
5 csbexg x y | ψ 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 φ y y = B [˙A / x]˙ ψ χ
20 elabgt B W y y = 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 χ