| Step | Hyp | Ref | Expression | 
						
							| 1 |  | dmwf |  |-  ( R e. U. ( R1 " On ) -> dom R e. U. ( R1 " On ) ) | 
						
							| 2 |  | rnwf |  |-  ( R e. U. ( R1 " On ) -> ran R e. U. ( R1 " On ) ) | 
						
							| 3 | 1 2 | jca |  |-  ( R e. U. ( R1 " On ) -> ( dom R e. U. ( R1 " On ) /\ ran R e. U. ( R1 " On ) ) ) | 
						
							| 4 |  | xpwf |  |-  ( ( dom R e. U. ( R1 " On ) /\ ran R e. U. ( R1 " On ) ) -> ( dom R X. ran R ) e. U. ( R1 " On ) ) | 
						
							| 5 |  | relssdmrn |  |-  ( Rel R -> R C_ ( dom R X. ran R ) ) | 
						
							| 6 |  | sswf |  |-  ( ( ( dom R X. ran R ) e. U. ( R1 " On ) /\ R C_ ( dom R X. ran R ) ) -> R e. U. ( R1 " On ) ) | 
						
							| 7 | 5 6 | sylan2 |  |-  ( ( ( dom R X. ran R ) e. U. ( R1 " On ) /\ Rel R ) -> R e. U. ( R1 " On ) ) | 
						
							| 8 | 7 | expcom |  |-  ( Rel R -> ( ( dom R X. ran R ) e. U. ( R1 " On ) -> R e. U. ( R1 " On ) ) ) | 
						
							| 9 | 4 8 | syl5 |  |-  ( Rel R -> ( ( dom R e. U. ( R1 " On ) /\ ran R e. U. ( R1 " On ) ) -> R e. U. ( R1 " On ) ) ) | 
						
							| 10 | 3 9 | impbid2 |  |-  ( Rel R -> ( R e. U. ( R1 " On ) <-> ( dom R e. U. ( R1 " On ) /\ ran R e. U. ( R1 " On ) ) ) ) |