Metamath Proof Explorer

Theorem prwf

Description: An unordered pair is well-founded if its elements are. (Contributed by Mario Carneiro, 10-Jun-2013) (Revised by Mario Carneiro, 17-Nov-2014)

Ref Expression
Assertion prwf 
|- ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) -> { A , B } e. U. ( R1 " On ) )

Proof

Step Hyp Ref Expression
1 df-pr 
 |-  { A , B } = ( { A } u. { B } )
2 snwf 
 |-  ( A e. U. ( R1 " On ) -> { A } e. U. ( R1 " On ) )
3 snwf 
 |-  ( B e. U. ( R1 " On ) -> { B } e. U. ( R1 " On ) )
4 unwf 
 |-  ( ( { A } e. U. ( R1 " On ) /\ { B } e. U. ( R1 " On ) ) <-> ( { A } u. { B } ) e. U. ( R1 " On ) )
5 4 biimpi 
 |-  ( ( { A } e. U. ( R1 " On ) /\ { B } e. U. ( R1 " On ) ) -> ( { A } u. { B } ) e. U. ( R1 " On ) )
6 2 3 5 syl2an 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) -> ( { A } u. { B } ) e. U. ( R1 " On ) )
7 1 6 eqeltrid 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) -> { A , B } e. U. ( R1 " On ) )