Metamath Proof Explorer


Theorem abfmpel

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

Ref Expression
Hypotheses abfmpel.1 F = x V y | φ
abfmpel.2 y | φ V
abfmpel.3 x = A y = B φ ψ
Assertion abfmpel A V B W B F A ψ

Proof

Step Hyp Ref Expression
1 abfmpel.1 F = x V y | φ
2 abfmpel.2 y | φ V
3 abfmpel.3 x = A y = B φ ψ
4 2 csbex A / x y | φ V
5 1 fvmpts A V A / x y | φ V F A = A / x y | φ
6 4 5 mpan2 A V F A = A / x y | φ
7 csbab A / x y | φ = y | [˙A / x]˙ φ
8 6 7 eqtrdi A V F A = y | [˙A / x]˙ φ
9 8 eleq2d A V B F A B y | [˙A / x]˙ φ
10 9 adantr A V B W B F A B y | [˙A / x]˙ φ
11 simpl A V y = B A V
12 3 ancoms y = B x = A φ ψ
13 12 adantll A V y = B x = A φ ψ
14 11 13 sbcied A V y = B [˙A / x]˙ φ ψ
15 14 ex A V y = B [˙A / x]˙ φ ψ
16 15 alrimiv A V y y = B [˙A / x]˙ φ ψ
17 elabgt B W y y = B [˙A / x]˙ φ ψ B y | [˙A / x]˙ φ ψ
18 16 17 sylan2 B W A V B y | [˙A / x]˙ φ ψ
19 18 ancoms A V B W B y | [˙A / x]˙ φ ψ
20 10 19 bitrd A V B W B F A ψ