Theorem bj-gabeqis

Description: Equality of generalized class abstractions, with implicit substitution. (Contributed by BJ, 4-Oct-2024)

	Ref	Expression
Hypotheses	bj-gabeqis.c	|- ( x = y -> A = B )
	bj-gabeqis.f	|- ( x = y -> ( ph <-> ps ) )
Assertion	bj-gabeqis	|- {{ A | x | ph }} = {{ B | y | ps }}

Proof

Step	Hyp	Ref	Expression
1		bj-gabeqis.c	|- ( x = y -> A = B )
2		bj-gabeqis.f	|- ( x = y -> ( ph <-> ps ) )
3	1	adantl	|- ( ( u = v /\ x = y ) -> A = B )
4		simpl	|- ( ( u = v /\ x = y ) -> u = v )
5	3 4	eqeq12d	|- ( ( u = v /\ x = y ) -> ( A = u <-> B = v ) )
6	2	adantl	|- ( ( u = v /\ x = y ) -> ( ph <-> ps ) )
7	5 6	anbi12d	|- ( ( u = v /\ x = y ) -> ( ( A = u /\ ph ) <-> ( B = v /\ ps ) ) )
8	7	cbvexdvaw	|- ( u = v -> ( E. x ( A = u /\ ph ) <-> E. y ( B = v /\ ps ) ) )
9	8	cbvabv	|- { u | E. x ( A = u /\ ph ) } = { v | E. y ( B = v /\ ps ) }
10		df-bj-gab	|- {{ A | x | ph }} = { u | E. x ( A = u /\ ph ) }
11		df-bj-gab	|- {{ B | y | ps }} = { v | E. y ( B = v /\ ps ) }
12	9 10 11	3eqtr4i	|- {{ A | x | ph }} = {{ B | y | ps }}