Theorem bj-adjg1

Description: Existence of the result of the adjunction (generalized only in the first term since this suffices for current applications). (Contributed by BJ, 19-Jan-2025) (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-adjg1	$$⊢A\in V\to A\cup \left\{x\right\}\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		uneq1	$$⊢y=A\to y\cup \left\{x\right\}=A\cup \left\{x\right\}$$
2	1	eleq1d	$$⊢y=A\to \left(y\cup \left\{x\right\}\in \mathrm{V}\leftrightarrow A\cup \left\{x\right\}\in \mathrm{V}\right)$$
3		ax-bj-adj	$$⊢\forall y\forall x\exists z\forall t\left(t\in z\leftrightarrow \left(t\in y\vee t=x\right)\right)$$
4	3	spi	$$⊢\forall x\exists z\forall t\left(t\in z\leftrightarrow \left(t\in y\vee t=x\right)\right)$$
5	4	spi	$$⊢\exists z\forall t\left(t\in z\leftrightarrow \left(t\in y\vee t=x\right)\right)$$
6		bj-axadj	$$⊢y\cup \left\{x\right\}\in \mathrm{V}\leftrightarrow \exists z\forall t\left(t\in z\leftrightarrow \left(t\in y\vee t=x\right)\right)$$
7	5 6	mpbir	$$⊢y\cup \left\{x\right\}\in \mathrm{V}$$
8	2 7	vtoclg	$$⊢A\in V\to A\cup \left\{x\right\}\in \mathrm{V}$$