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	⊢ ( ¬ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ⟨ 𝐴 , 𝐵 ⟩ = ∅ )

Proof

Step	Hyp	Ref	Expression
1		dfopif	⊢ ⟨ 𝐴 , 𝐵 ⟩ = if ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) , { { 𝐴 } , { 𝐴 , 𝐵 } } , ∅ )
2		iffalse	⊢ ( ¬ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → if ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) , { { 𝐴 } , { 𝐴 , 𝐵 } } , ∅ ) = ∅ )
3	1 2	syl5eq	⊢ ( ¬ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ⟨ 𝐴 , 𝐵 ⟩ = ∅ )