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