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 ) )