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

Metamath Proof Explorer

Theorem elabgt

Description: Membership in a class abstraction, using implicit substitution. (Closed theorem version of elabg .) (Contributed by NM, 7-Nov-2005) (Proof shortened by Andrew Salmon, 8-Jun-2011) Reduce axiom usage. (Revised by GG, 12-Oct-2024) (Proof shortened by Wolf Lammen, 11-May-2025) (Proof shortened by SN, 1-Dec-2025)

Ref Expression
Assertion elabgt 
|- ( ( A e. B /\ A. x ( x = A -> ( ph <-> ps ) ) ) -> ( A e. { x | ph } <-> ps ) )

Proof

Step Hyp Ref Expression
1 elab6g 
 |-  ( A e. B -> ( A e. { x | ph } <-> A. x ( x = A -> ph ) ) )
2 pm5.74 
 |-  ( ( x = A -> ( ph <-> ps ) ) <-> ( ( x = A -> ph ) <-> ( x = A -> ps ) ) )
3 2 biimpi 
 |-  ( ( x = A -> ( ph <-> ps ) ) -> ( ( x = A -> ph ) <-> ( x = A -> ps ) ) )
4 3 alimi 
 |-  ( A. x ( x = A -> ( ph <-> ps ) ) -> A. x ( ( x = A -> ph ) <-> ( x = A -> ps ) ) )
5 albi 
 |-  ( A. x ( ( x = A -> ph ) <-> ( x = A -> ps ) ) -> ( A. x ( x = A -> ph ) <-> A. x ( x = A -> ps ) ) )
6 4 5 syl 
 |-  ( A. x ( x = A -> ( ph <-> ps ) ) -> ( A. x ( x = A -> ph ) <-> A. x ( x = A -> ps ) ) )
7 1 6 sylan9bb 
 |-  ( ( A e. B /\ A. x ( x = A -> ( ph <-> ps ) ) ) -> ( A e. { x | ph } <-> A. x ( x = A -> ps ) ) )
8 19.23v 
 |-  ( A. x ( x = A -> ps ) <-> ( E. x x = A -> ps ) )
9 elisset 
 |-  ( A e. B -> E. x x = A )
10 pm5.5 
 |-  ( E. x x = A -> ( ( E. x x = A -> ps ) <-> ps ) )
11 9 10 syl 
 |-  ( A e. B -> ( ( E. x x = A -> ps ) <-> ps ) )
12 8 11 bitrid 
 |-  ( A e. B -> ( A. x ( x = A -> ps ) <-> ps ) )
13 12 adantr 
 |-  ( ( A e. B /\ A. x ( x = A -> ( ph <-> ps ) ) ) -> ( A. x ( x = A -> ps ) <-> ps ) )
14 7 13 bitrd 
 |-  ( ( A e. B /\ A. x ( x = A -> ( ph <-> ps ) ) ) -> ( A e. { x | ph } <-> ps ) )