Metamath Proof Explorer

Theorem bj-prfromadj

Description: Unordered pair from adjunction. (Contributed by BJ, 19-Jan-2025) (Proof modification is discouraged.)

Ref Expression
Assertion bj-prfromadj 
|- { x , y } e. _V

Proof

Step Hyp Ref Expression
1 df-pr 
 |-  { x , y } = ( { x } u. { y } )
2 bj-snfromadj 
 |-  { x } e. _V
3 bj-adjg1 
 |-  ( { x } e. _V -> ( { x } u. { y } ) e. _V )
4 2 3 ax-mp 
 |-  ( { x } u. { y } ) e. _V
5 1 4 eqeltri 
 |-  { x , y } e. _V