bj-gabss

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

		Ref	Expression
	Assertion	bj-gabss	$⊢ \forall x (A = B \land (φ \to ψ)) \to {{A \| x \| φ}} \subseteq {{B \| x \| ψ}}$

Step	Hyp	Ref	Expression
1		eqeq1	$⊢ A = B \to (A = y \leftrightarrow B = y)$
2	1	biimpd	$⊢ A = B \to (A = y \to B = y)$
3	2	adantr	$⊢ (A = B \land (φ \to ψ)) \to (A = y \to B = y)$
4		simpr	$⊢ (A = B \land (φ \to ψ)) \to (φ \to ψ)$
5	3 4	anim12d	$⊢ (A = B \land (φ \to ψ)) \to ((A = y \land φ) \to (B = y \land ψ))$
6	5	aleximi	$⊢ \forall x (A = B \land (φ \to ψ)) \to (\exists x (A = y \land φ) \to \exists x (B = y \land ψ))$
7	6	alrimiv	$⊢ \forall x (A = B \land (φ \to ψ)) \to \forall y (\exists x (A = y \land φ) \to \exists x (B = y \land ψ))$
8		ss2ab	$⊢ \{y \| \exists x (A = y \land φ)\} \subseteq \{y \| \exists x (B = y \land ψ)\} \leftrightarrow \forall y (\exists x (A = y \land φ) \to \exists x (B = y \land ψ))$
9	7 8	sylibr	$⊢ \forall x (A = B \land (φ \to ψ)) \to \{y \| \exists x (A = y \land φ)\} \subseteq \{y \| \exists x (B = y \land ψ)\}$
10		df-bj-gab	$⊢ {{A \| x \| φ}} = \{y \| \exists x (A = y \land φ)\}$
11		df-bj-gab	$⊢ {{B \| x \| ψ}} = \{y \| \exists x (B = y \land ψ)\}$
12	9 10 11	3sstr4g	$⊢ \forall x (A = B \land (φ \to ψ)) \to {{A \| x \| φ}} \subseteq {{B \| x \| ψ}}$

Metamath Proof Explorer