Theorem bj-gabeqd

Description: Equality of generalized class abstractions. Deduction form. (Contributed by BJ, 4-Oct-2024)

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

Proof

Step	Hyp	Ref	Expression
1		bj-gabeqd.nf	|- ( ph -> A. x ph )
2		bj-gabeqd.c	|- ( ph -> A = B )
3		bj-gabeqd.f	|- ( ph -> ( ps <-> ch ) )
4	3	biimpd	|- ( ph -> ( ps -> ch ) )
5	1 2 4	bj-gabssd	|- ( ph -> {{ A | x | ps }} C_ {{ B | x | ch }} )
6	2	eqcomd	|- ( ph -> B = A )
7	3	biimprd	|- ( ph -> ( ch -> ps ) )
8	1 6 7	bj-gabssd	|- ( ph -> {{ B | x | ch }} C_ {{ A | x | ps }} )
9	5 8	eqssd	|- ( ph -> {{ A | x | ps }} = {{ B | x | ch }} )