Metamath Proof Explorer

Theorem bj-elgab

Description: Elements of a generalized class abstraction. (Contributed by BJ, 4-Oct-2024)

Ref Expression
Hypotheses bj-elgab.nf 
|- ( ph -> A. x ph )
bj-elgab.nfa 
|- ( ph -> F/_ x A )
bj-elgab.ex 
|- ( ph -> A e. V )
bj-elgab.is 
|- ( ph -> ( E. x ( A = B /\ ps ) <-> ch ) )
Assertion bj-elgab 
|- ( ph -> ( A e. {{ B | x | ps }} <-> ch ) )

Proof

Step Hyp Ref Expression
1 bj-elgab.nf 
 |-  ( ph -> A. x ph )
2 bj-elgab.nfa 
 |-  ( ph -> F/_ x A )
3 bj-elgab.ex 
 |-  ( ph -> A e. V )
4 bj-elgab.is 
 |-  ( ph -> ( E. x ( A = B /\ ps ) <-> ch ) )
5 df-bj-gab 
 |-  {{ B | x | ps }} = { y | E. x ( B = y /\ ps ) }
6 5 eleq2i 
 |-  ( A e. {{ B | x | ps }} <-> A e. { y | E. x ( B = y /\ ps ) } )
7 1 adantr 
 |-  ( ( ph /\ y = A ) -> A. x ph )
8 nfcvd 
 |-  ( F/_ x A -> F/_ x y )
9 id 
 |-  ( F/_ x A -> F/_ x A )
10 8 9 nfeqd 
 |-  ( F/_ x A -> F/ x y = A )
11 10 nf5rd 
 |-  ( F/_ x A -> ( y = A -> A. x y = A ) )
12 2 11 syl 
 |-  ( ph -> ( y = A -> A. x y = A ) )
13 12 imp 
 |-  ( ( ph /\ y = A ) -> A. x y = A )
14 19.26 
 |-  ( A. x ( ph /\ y = A ) <-> ( A. x ph /\ A. x y = A ) )
15 7 13 14 sylanbrc 
 |-  ( ( ph /\ y = A ) -> A. x ( ph /\ y = A ) )
16 eqeq2 
 |-  ( y = A -> ( B = y <-> B = A ) )
17 eqcom 
 |-  ( B = A <-> A = B )
18 16 17 bitrdi 
 |-  ( y = A -> ( B = y <-> A = B ) )
19 18 anbi1d 
 |-  ( y = A -> ( ( B = y /\ ps ) <-> ( A = B /\ ps ) ) )
20 19 adantl 
 |-  ( ( ph /\ y = A ) -> ( ( B = y /\ ps ) <-> ( A = B /\ ps ) ) )
21 15 20 exbidh 
 |-  ( ( ph /\ y = A ) -> ( E. x ( B = y /\ ps ) <-> E. x ( A = B /\ ps ) ) )
22 21 ex 
 |-  ( ph -> ( y = A -> ( E. x ( B = y /\ ps ) <-> E. x ( A = B /\ ps ) ) ) )
23 22 alrimiv 
 |-  ( ph -> A. y ( y = A -> ( E. x ( B = y /\ ps ) <-> E. x ( A = B /\ ps ) ) ) )
24 elabgt 
 |-  ( ( A e. V /\ A. y ( y = A -> ( E. x ( B = y /\ ps ) <-> E. x ( A = B /\ ps ) ) ) ) -> ( A e. { y | E. x ( B = y /\ ps ) } <-> E. x ( A = B /\ ps ) ) )
25 3 23 24 syl2anc 
 |-  ( ph -> ( A e. { y | E. x ( B = y /\ ps ) } <-> E. x ( A = B /\ ps ) ) )
26 25 4 bitrd 
 |-  ( ph -> ( A e. { y | E. x ( B = y /\ ps ) } <-> ch ) )
27 6 26 syl5bb 
 |-  ( ph -> ( A e. {{ B | x | ps }} <-> ch ) )