Theorem elmptrab2

Description: Membership in a one-parameter class of sets, indexed by arbitrary base sets. (Contributed by Stefan O'Rear, 28-Jul-2015) (Revised by AV, 26-Mar-2021)

	Ref	Expression
Hypotheses	elmptrab2.f	|- F = ( x e. _V |-> { y e. B | ph } )
	elmptrab2.s1	|- ( ( x = X /\ y = Y ) -> ( ph <-> ps ) )
	elmptrab2.s2	|- ( x = X -> B = C )
	elmptrab2.ex	|- B e. _V
	elmptrab2.rc	|- ( Y e. C -> X e. W )
Assertion	elmptrab2	|- ( Y e. ( F ` X ) <-> ( Y e. C /\ ps ) )

Proof

Step	Hyp	Ref	Expression
1		elmptrab2.f	|- F = ( x e. _V |-> { y e. B | ph } )
2		elmptrab2.s1	|- ( ( x = X /\ y = Y ) -> ( ph <-> ps ) )
3		elmptrab2.s2	|- ( x = X -> B = C )
4		elmptrab2.ex	|- B e. _V
5		elmptrab2.rc	|- ( Y e. C -> X e. W )
6	4	a1i	|- ( x e. _V -> B e. _V )
7	1 2 3 6	elmptrab	|- ( Y e. ( F ` X ) <-> ( X e. _V /\ Y e. C /\ ps ) )
8		3simpc	|- ( ( X e. _V /\ Y e. C /\ ps ) -> ( Y e. C /\ ps ) )
9	5	elexd	|- ( Y e. C -> X e. _V )
10	9	adantr	|- ( ( Y e. C /\ ps ) -> X e. _V )
11		simpl	|- ( ( Y e. C /\ ps ) -> Y e. C )
12		simpr	|- ( ( Y e. C /\ ps ) -> ps )
13	10 11 12	3jca	|- ( ( Y e. C /\ ps ) -> ( X e. _V /\ Y e. C /\ ps ) )
14	8 13	impbii	|- ( ( X e. _V /\ Y e. C /\ ps ) <-> ( Y e. C /\ ps ) )
15	7 14	bitri	|- ( Y e. ( F ` X ) <-> ( Y e. C /\ ps ) )