Theorem elnonrel

Description: Only an ordered pair where not both entries are sets could be an element of the non-relation part of class. (Contributed by RP, 25-Oct-2020)

	Ref	Expression
Assertion	elnonrel	⊢ ( ⟨ 𝑋 , 𝑌 ⟩ ∈ ( 𝐴 ∖ ◡ ◡ 𝐴 ) ↔ ( ∅ ∈ 𝐴 ∧ ¬ ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ) )

Proof

Step	Hyp	Ref	Expression
1		nonrel	⊢ ( 𝐴 ∖ ◡ ◡ 𝐴 ) = ( 𝐴 ∖ ( V × V ) )
2	1	eleq2i	⊢ ( ⟨ 𝑋 , 𝑌 ⟩ ∈ ( 𝐴 ∖ ◡ ◡ 𝐴 ) ↔ ⟨ 𝑋 , 𝑌 ⟩ ∈ ( 𝐴 ∖ ( V × V ) ) )
3		eldif	⊢ ( ⟨ 𝑋 , 𝑌 ⟩ ∈ ( 𝐴 ∖ ( V × V ) ) ↔ ( ⟨ 𝑋 , 𝑌 ⟩ ∈ 𝐴 ∧ ¬ ⟨ 𝑋 , 𝑌 ⟩ ∈ ( V × V ) ) )
4		opelxp	⊢ ( ⟨ 𝑋 , 𝑌 ⟩ ∈ ( V × V ) ↔ ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) )
5	4	notbii	⊢ ( ¬ ⟨ 𝑋 , 𝑌 ⟩ ∈ ( V × V ) ↔ ¬ ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) )
6	5	anbi2i	⊢ ( ( ⟨ 𝑋 , 𝑌 ⟩ ∈ 𝐴 ∧ ¬ ⟨ 𝑋 , 𝑌 ⟩ ∈ ( V × V ) ) ↔ ( ⟨ 𝑋 , 𝑌 ⟩ ∈ 𝐴 ∧ ¬ ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ) )
7		opprc	⊢ ( ¬ ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → ⟨ 𝑋 , 𝑌 ⟩ = ∅ )
8	7	eleq1d	⊢ ( ¬ ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → ( ⟨ 𝑋 , 𝑌 ⟩ ∈ 𝐴 ↔ ∅ ∈ 𝐴 ) )
9	8	pm5.32ri	⊢ ( ( ⟨ 𝑋 , 𝑌 ⟩ ∈ 𝐴 ∧ ¬ ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ) ↔ ( ∅ ∈ 𝐴 ∧ ¬ ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ) )
10	6 9	bitri	⊢ ( ( ⟨ 𝑋 , 𝑌 ⟩ ∈ 𝐴 ∧ ¬ ⟨ 𝑋 , 𝑌 ⟩ ∈ ( V × V ) ) ↔ ( ∅ ∈ 𝐴 ∧ ¬ ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ) )
11	3 10	bitri	⊢ ( ⟨ 𝑋 , 𝑌 ⟩ ∈ ( 𝐴 ∖ ( V × V ) ) ↔ ( ∅ ∈ 𝐴 ∧ ¬ ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ) )
12	2 11	bitri	⊢ ( ⟨ 𝑋 , 𝑌 ⟩ ∈ ( 𝐴 ∖ ◡ ◡ 𝐴 ) ↔ ( ∅ ∈ 𝐴 ∧ ¬ ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ) )