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