Theorem 0nelopab

Description: The empty set is never an element in an ordered-pair class abstraction. (Contributed by Alexander van der Vekens, 5-Nov-2017) Reduce axiom usage and shorten proof. (Revised by GG, 3-Oct-2024)

	Ref	Expression
Assertion	0nelopab	⊢ ¬ ∅ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }

Proof

Step	Hyp	Ref	Expression
1		vex	⊢ 𝑥 ∈ V
2		vex	⊢ 𝑦 ∈ V
3	1 2	opnzi	⊢ ⟨ 𝑥 , 𝑦 ⟩ ≠ ∅
4	3	nesymi	⊢ ¬ ∅ = ⟨ 𝑥 , 𝑦 ⟩
5	4	intnanr	⊢ ¬ ( ∅ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 )
6	5	nex	⊢ ¬ ∃ 𝑦 ( ∅ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 )
7	6	nex	⊢ ¬ ∃ 𝑥 ∃ 𝑦 ( ∅ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 )
8		elopab	⊢ ( ∅ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ ∃ 𝑥 ∃ 𝑦 ( ∅ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) )
9	7 8	mtbir	⊢ ¬ ∅ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }