Metamath Proof Explorer

Theorem opprc

Description: Expansion of an ordered pair when either member is a proper class. (Contributed by Mario Carneiro, 26-Apr-2015)

		Ref	Expression
	Assertion	opprc	\|- ( -. ( A e. _V /\ B e. _V ) -> <. A , B >. = (/) )

Step	Hyp	Ref	Expression
1		dfopif	\|- <. A , B >. = if ( ( A e. _V /\ B e. _V ) , { { A } , { A , B } } , (/) )
2		iffalse	\|- ( -. ( A e. _V /\ B e. _V ) -> if ( ( A e. _V /\ B e. _V ) , { { A } , { A , B } } , (/) ) = (/) )
3	1 2	eqtrid	\|- ( -. ( A e. _V /\ B e. _V ) -> <. A , B >. = (/) )

Step

Hyp

Ref

Expression

 |-  <. A , B >. = if ( ( A e. _V /\ B e. _V ) , { { A } , { A , B } } , (/) )

 |-  ( -. ( A e. _V /\ B e. _V ) -> if ( ( A e. _V /\ B e. _V ) , { { A } , { A , B } } , (/) ) = (/) )

1 2

 |-  ( -. ( A e. _V /\ B e. _V ) -> <. A , B >. = (/) )