This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 e. V |-> { y | ph } )
abfmpel.2 
|- { y | ph } e. _V
abfmpel.3 
|- ( ( x = A /\ y = B ) -> ( ph <-> ps ) )
Assertion abfmpel 
|- ( ( A e. V /\ B e. W ) -> ( B e. ( F ` A ) <-> ps ) )

Proof

Step Hyp Ref Expression
1 abfmpel.1 
 |-  F = ( x e. V |-> { y | ph } )
2 abfmpel.2 
 |-  { y | ph } e. _V
3 abfmpel.3 
 |-  ( ( x = A /\ y = B ) -> ( ph <-> ps ) )
4 2 csbex 
 |-  [_ A / x ]_ { y | ph } e. _V
5 1 fvmpts 
 |-  ( ( A e. V /\ [_ A / x ]_ { y | ph } e. _V ) -> ( F ` A ) = [_ A / x ]_ { y | ph } )
6 4 5 mpan2 
 |-  ( A e. V -> ( F ` A ) = [_ A / x ]_ { y | ph } )
7 csbab 
 |-  [_ A / x ]_ { y | ph } = { y | [. A / x ]. ph }
8 6 7 eqtrdi 
 |-  ( A e. V -> ( F ` A ) = { y | [. A / x ]. ph } )
9 8 eleq2d 
 |-  ( A e. V -> ( B e. ( F ` A ) <-> B e. { y | [. A / x ]. ph } ) )
10 9 adantr 
 |-  ( ( A e. V /\ B e. W ) -> ( B e. ( F ` A ) <-> B e. { y | [. A / x ]. ph } ) )
11 simpl 
 |-  ( ( A e. V /\ y = B ) -> A e. V )
12 3 ancoms 
 |-  ( ( y = B /\ x = A ) -> ( ph <-> ps ) )
13 12 adantll 
 |-  ( ( ( A e. V /\ y = B ) /\ x = A ) -> ( ph <-> ps ) )
14 11 13 sbcied 
 |-  ( ( A e. V /\ y = B ) -> ( [. A / x ]. ph <-> ps ) )
15 14 ex 
 |-  ( A e. V -> ( y = B -> ( [. A / x ]. ph <-> ps ) ) )
16 15 alrimiv 
 |-  ( A e. V -> A. y ( y = B -> ( [. A / x ]. ph <-> ps ) ) )
17 elabgt 
 |-  ( ( B e. W /\ A. y ( y = B -> ( [. A / x ]. ph <-> ps ) ) ) -> ( B e. { y | [. A / x ]. ph } <-> ps ) )
18 16 17 sylan2 
 |-  ( ( B e. W /\ A e. V ) -> ( B e. { y | [. A / x ]. ph } <-> ps ) )
19 18 ancoms 
 |-  ( ( A e. V /\ B e. W ) -> ( B e. { y | [. A / x ]. ph } <-> ps ) )
20 10 19 bitrd 
 |-  ( ( A e. V /\ B e. W ) -> ( B e. ( F ` A ) <-> ps ) )