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	Could not format assertion : No typesetting found for |- {{ A | x | ph }} = {{ B | y | ps }} with typecode |-

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	Could not format {{ A | x | ph }} = { u | E. x ( A = u /\ ph ) } : No typesetting found for |- {{ A | x | ph }} = { u | E. x ( A = u /\ ph ) } with typecode |-
11		df-bj-gab	Could not format {{ B | y | ps }} = { v | E. y ( B = v /\ ps ) } : No typesetting found for |- {{ B | y | ps }} = { v | E. y ( B = v /\ ps ) } with typecode |-
12	9 10 11	3eqtr4i	Could not format {{ A | x | ph }} = {{ B | y | ps }} : No typesetting found for |- {{ A | x | ph }} = {{ B | y | ps }} with typecode |-