This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∈ V ∧ B ∈ V → A B = ∅

Proof

Step Hyp Ref Expression
1 dfopif ⊢ A B = if A ∈ V ∧ B ∈ V A A B ∅
2 iffalse ⊢ ¬ A ∈ V ∧ B ∈ V → if A ∈ V ∧ B ∈ V A A B ∅ = ∅
3 1 2 eqtrid ⊢ ¬ A ∈ V ∧ B ∈ V → A B = ∅