Theorem opprc2

Description: Expansion of an ordered pair when the second member is a proper class. See also opprc . (Contributed by NM, 15-Nov-1994) (Revised by Mario Carneiro, 26-Apr-2015)

	Ref	Expression
Assertion	opprc2	⊢ ( ¬ 𝐵 ∈ V → ⟨ 𝐴 , 𝐵 ⟩ = ∅ )

Proof

Step	Hyp	Ref	Expression
1		simpr	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → 𝐵 ∈ V )
2		opprc	⊢ ( ¬ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ⟨ 𝐴 , 𝐵 ⟩ = ∅ )
3	1 2	nsyl5	⊢ ( ¬ 𝐵 ∈ V → ⟨ 𝐴 , 𝐵 ⟩ = ∅ )