Theorem bj-gabss

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

	Ref	Expression
Assertion	bj-gabss	Could not format assertion : No typesetting found for |- ( A. x ( A = B /\ ( ph -> ps ) ) -> {{ A | x | ph }} C_ {{ B | x | ps }} ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		eqeq1	$$⊢A=B\to \left(A=y\leftrightarrow B=y\right)$$
2	1	biimpd	$$⊢A=B\to \left(A=y\to B=y\right)$$
3	2	adantr	$$⊢\left(A=B\wedge \left(\phi \to \psi \right)\right)\to \left(A=y\to B=y\right)$$
4		simpr	$$⊢\left(A=B\wedge \left(\phi \to \psi \right)\right)\to \left(\phi \to \psi \right)$$
5	3 4	anim12d	$$⊢\left(A=B\wedge \left(\phi \to \psi \right)\right)\to \left(\left(A=y\wedge \phi \right)\to \left(B=y\wedge \psi \right)\right)$$
6	5	aleximi	$$⊢\forall x\left(A=B\wedge \left(\phi \to \psi \right)\right)\to \left(\exists x\left(A=y\wedge \phi \right)\to \exists x\left(B=y\wedge \psi \right)\right)$$
7	6	alrimiv	$$⊢\forall x\left(A=B\wedge \left(\phi \to \psi \right)\right)\to \forall y\left(\exists x\left(A=y\wedge \phi \right)\to \exists x\left(B=y\wedge \psi \right)\right)$$
8		ss2ab	$$⊢\left\{y|\exists x\left(A=y\wedge \phi \right)\right\}\subseteq \left\{y|\exists x\left(B=y\wedge \psi \right)\right\}\leftrightarrow \forall y\left(\exists x\left(A=y\wedge \phi \right)\to \exists x\left(B=y\wedge \psi \right)\right)$$
9	7 8	sylibr	$$⊢\forall x\left(A=B\wedge \left(\phi \to \psi \right)\right)\to \left\{y|\exists x\left(A=y\wedge \phi \right)\right\}\subseteq \left\{y|\exists x\left(B=y\wedge \psi \right)\right\}$$
10		df-bj-gab	Could not format {{ A | x | ph }} = { y | E. x ( A = y /\ ph ) } : No typesetting found for |- {{ A | x | ph }} = { y | E. x ( A = y /\ ph ) } with typecode |-
11		df-bj-gab	Could not format {{ B | x | ps }} = { y | E. x ( B = y /\ ps ) } : No typesetting found for |- {{ B | x | ps }} = { y | E. x ( B = y /\ ps ) } with typecode |-
12	9 10 11	3sstr4g	Could not format ( A. x ( A = B /\ ( ph -> ps ) ) -> {{ A | x | ph }} C_ {{ B | x | ps }} ) : No typesetting found for |- ( A. x ( A = B /\ ( ph -> ps ) ) -> {{ A | x | ph }} C_ {{ B | x | ps }} ) with typecode |-