Theorem bj-axadj

Description: Two ways of stating the axiom of adjunction (which is the universal closure of either side, see ax-bj-adj ). (Contributed by BJ, 12-Jan-2025) (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-axadj	$$⊢x\cup \left\{y\right\}\in \mathrm{V}\leftrightarrow \exists z\forall t\left(t\in z\leftrightarrow \left(t\in x\vee t=y\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		elun	$$⊢t\in \left(x\cup \left\{y\right\}\right)\leftrightarrow \left(t\in x\vee t\in \left\{y\right\}\right)$$
2		velsn	$$⊢t\in \left\{y\right\}\leftrightarrow t=y$$
3	2	orbi2i	$$⊢\left(t\in x\vee t\in \left\{y\right\}\right)\leftrightarrow \left(t\in x\vee t=y\right)$$
4	1 3	bitri	$$⊢t\in \left(x\cup \left\{y\right\}\right)\leftrightarrow \left(t\in x\vee t=y\right)$$
5	4	bj-clex	$$⊢x\cup \left\{y\right\}\in \mathrm{V}\leftrightarrow \exists z\forall t\left(t\in z\leftrightarrow \left(t\in x\vee t=y\right)\right)$$