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)

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

Proof

Step	Hyp	Ref	Expression
1		elopab	⊢ ( ∅ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ ∃ 𝑥 ∃ 𝑦 ( ∅ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) )
2		nfopab1	⊢ Ⅎ 𝑥 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }
3	2	nfel2	⊢ Ⅎ 𝑥 ∅ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }
4	3	nfn	⊢ Ⅎ 𝑥 ¬ ∅ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }
5		nfopab2	⊢ Ⅎ 𝑦 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }
6	5	nfel2	⊢ Ⅎ 𝑦 ∅ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }
7	6	nfn	⊢ Ⅎ 𝑦 ¬ ∅ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }
8		vex	⊢ 𝑥 ∈ V
9		vex	⊢ 𝑦 ∈ V
10	8 9	opnzi	⊢ ⟨ 𝑥 , 𝑦 ⟩ ≠ ∅
11		nesym	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ≠ ∅ ↔ ¬ ∅ = ⟨ 𝑥 , 𝑦 ⟩ )
12		pm2.21	⊢ ( ¬ ∅ = ⟨ 𝑥 , 𝑦 ⟩ → ( ∅ = ⟨ 𝑥 , 𝑦 ⟩ → ¬ ∅ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ) )
13	11 12	sylbi	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ≠ ∅ → ( ∅ = ⟨ 𝑥 , 𝑦 ⟩ → ¬ ∅ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ) )
14	10 13	ax-mp	⊢ ( ∅ = ⟨ 𝑥 , 𝑦 ⟩ → ¬ ∅ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } )
15	14	adantr	⊢ ( ( ∅ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) → ¬ ∅ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } )
16	7 15	exlimi	⊢ ( ∃ 𝑦 ( ∅ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) → ¬ ∅ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } )
17	4 16	exlimi	⊢ ( ∃ 𝑥 ∃ 𝑦 ( ∅ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) → ¬ ∅ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } )
18	1 17	sylbi	⊢ ( ∅ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } → ¬ ∅ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } )
19		id	⊢ ( ¬ ∅ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } → ¬ ∅ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } )
20	18 19	pm2.61i	⊢ ¬ ∅ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }