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\to A=B$$
	bj-gabeqis.f	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	bj-gabeqis	$$⊢{{A\left|x\right|\phi }}={{B\left|y\right|\psi }}$$

Proof

Step	Hyp	Ref	Expression
1		bj-gabeqis.c	$$⊢x=y\to A=B$$
2		bj-gabeqis.f	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
3	1	adantl	$$⊢\left(u=v\wedge x=y\right)\to A=B$$
4		simpl	$$⊢\left(u=v\wedge x=y\right)\to u=v$$
5	3 4	eqeq12d	$$⊢\left(u=v\wedge x=y\right)\to \left(A=u\leftrightarrow B=v\right)$$
6	2	adantl	$$⊢\left(u=v\wedge x=y\right)\to \left(\phi \leftrightarrow \psi \right)$$
7	5 6	anbi12d	$$⊢\left(u=v\wedge x=y\right)\to \left(\left(A=u\wedge \phi \right)\leftrightarrow \left(B=v\wedge \psi \right)\right)$$
8	7	cbvexdvaw	$$⊢u=v\to \left(\exists x\left(A=u\wedge \phi \right)\leftrightarrow \exists y\left(B=v\wedge \psi \right)\right)$$
9	8	cbvabv	$$⊢\left\{u|\exists x\left(A=u\wedge \phi \right)\right\}=\left\{v|\exists y\left(B=v\wedge \psi \right)\right\}$$
10		df-bj-gab	$$⊢{{A\left|x\right|\phi }}=\left\{u|\exists x\left(A=u\wedge \phi \right)\right\}$$
11		df-bj-gab	$$⊢{{B\left|y\right|\psi }}=\left\{v|\exists y\left(B=v\wedge \psi \right)\right\}$$
12	9 10 11	3eqtr4i	$$⊢{{A\left|x\right|\phi }}={{B\left|y\right|\psi }}$$