Metamath Proof Explorer

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 ⊢ x ∪ y ∈ V

Proof

Step Hyp Ref Expression
1 vex ⊢ x ∈ V
2 bj-snexg ⊢ y ∈ V → y ∈ V
3 2 elv ⊢ y ∈ V
4 bj-unexg ⊢ x ∈ V ∧ y ∈ V → x ∪ y ∈ V
5 1 3 4 mp2an ⊢ x ∪ y ∈ V