Metamath Proof Explorer


Theorem 0nelopabOLD

Description: Obsolete version of 0nelopab as of 3-Oct-2024. (Contributed by Alexander van der Vekens, 5-Nov-2017) (Proof modification is discouraged.) (New usage is discouraged.)

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

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 ¬ ∅ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }