Theorem opwf

Description: An ordered pair is well-founded if its elements are. (Contributed by Mario Carneiro, 10-Jun-2013)

	Ref	Expression
Assertion	opwf	|- ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) -> <. A , B >. e. U. ( R1 " On ) )

Proof

Step	Hyp	Ref	Expression
1		dfopg	|- ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) -> <. A , B >. = { { A } , { A , B } } )
2		snwf	|- ( A e. U. ( R1 " On ) -> { A } e. U. ( R1 " On ) )
3		prwf	|- ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) -> { A , B } e. U. ( R1 " On ) )
4		prwf	|- ( ( { A } e. U. ( R1 " On ) /\ { A , B } e. U. ( R1 " On ) ) -> { { A } , { A , B } } e. U. ( R1 " On ) )
5	2 3 4	syl2an2r	|- ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) -> { { A } , { A , B } } e. U. ( R1 " On ) )
6	1 5	eqeltrd	|- ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) -> <. A , B >. e. U. ( R1 " On ) )