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 u. { y } ) e. _V

Proof

Step Hyp Ref Expression
1 vex 
 |-  x e. _V
2 bj-snexg 
 |-  ( y e. _V -> { y } e. _V )
3 2 elv 
 |-  { y } e. _V
4 bj-unexg 
 |-  ( ( x e. _V /\ { y } e. _V ) -> ( x u. { y } ) e. _V )
5 1 3 4 mp2an 
 |-  ( x u. { y } ) e. _V