Theorem bj-adjfrombun

Description: Adjunction from singleton and binary union. (Contributed by BJ, 19-Jan-2025) (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-adjfrombun	⊢ ( 𝑥 ∪ { 𝑦 } ) ∈ V

Proof

Step	Hyp	Ref	Expression
1		vex	⊢ 𝑥 ∈ V
2		bj-snexg	⊢ ( 𝑦 ∈ V → { 𝑦 } ∈ V )
3	2	elv	⊢ { 𝑦 } ∈ V
4		bj-unexg	⊢ ( ( 𝑥 ∈ V ∧ { 𝑦 } ∈ V ) → ( 𝑥 ∪ { 𝑦 } ) ∈ V )
5	1 3 4	mp2an	⊢ ( 𝑥 ∪ { 𝑦 } ) ∈ V