Theorem unabw

Description: Union of two class abstractions. Version of unab using implicit substitution, which does not require ax-8 , ax-10 , ax-12 . (Contributed by GG, 15-Oct-2024)

	Ref	Expression
Hypotheses	unabw.1	$$⊢x=y\to \left(\phi \leftrightarrow \chi \right)$$
	unabw.2	$$⊢x=y\to \left(\psi \leftrightarrow \theta \right)$$
Assertion	unabw	$$⊢\left\{x|\phi \right\}\cup \left\{x|\psi \right\}=\left\{y|\left(\chi \vee \theta \right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		unabw.1	$$⊢x=y\to \left(\phi \leftrightarrow \chi \right)$$
2		unabw.2	$$⊢x=y\to \left(\psi \leftrightarrow \theta \right)$$
3		df-un	$$⊢\left\{x|\phi \right\}\cup \left\{x|\psi \right\}=\left\{y|\left(y\in \left\{x|\phi \right\}\vee y\in \left\{x|\psi \right\}\right)\right\}$$
4		df-clab	$$⊢y\in \left\{x|\phi \right\}\leftrightarrow \left[y/x\right]\phi$$
5	1	sbievw	$$⊢\left[y/x\right]\phi \leftrightarrow \chi$$
6	4 5	bitri	$$⊢y\in \left\{x|\phi \right\}\leftrightarrow \chi$$
7		df-clab	$$⊢y\in \left\{x|\psi \right\}\leftrightarrow \left[y/x\right]\psi$$
8	2	sbievw	$$⊢\left[y/x\right]\psi \leftrightarrow \theta$$
9	7 8	bitri	$$⊢y\in \left\{x|\psi \right\}\leftrightarrow \theta$$
10	6 9	orbi12i	$$⊢\left(y\in \left\{x|\phi \right\}\vee y\in \left\{x|\psi \right\}\right)\leftrightarrow \left(\chi \vee \theta \right)$$
11	10	abbii	$$⊢\left\{y|\left(y\in \left\{x|\phi \right\}\vee y\in \left\{x|\psi \right\}\right)\right\}=\left\{y|\left(\chi \vee \theta \right)\right\}$$
12	3 11	eqtri	$$⊢\left\{x|\phi \right\}\cup \left\{x|\psi \right\}=\left\{y|\left(\chi \vee \theta \right)\right\}$$