Description: Obsolete version of cnv0 as of 31-Jan-2026. (Contributed by NM, 6-Apr-1998) Remove dependency on ax-sep , ax-nul , ax-pr . (Revised by KP, 25-Oct-2021) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | cnv0OLD | ⊢ ◡ ∅ = ∅ |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | br0 | ⊢ ¬ 𝑦 ∅ 𝑧 | |
| 2 | 1 | intnan | ⊢ ¬ ( 𝑥 = ⟨ 𝑧 , 𝑦 ⟩ ∧ 𝑦 ∅ 𝑧 ) |
| 3 | 2 | nex | ⊢ ¬ ∃ 𝑦 ( 𝑥 = ⟨ 𝑧 , 𝑦 ⟩ ∧ 𝑦 ∅ 𝑧 ) |
| 4 | 3 | nex | ⊢ ¬ ∃ 𝑧 ∃ 𝑦 ( 𝑥 = ⟨ 𝑧 , 𝑦 ⟩ ∧ 𝑦 ∅ 𝑧 ) |
| 5 | df-cnv | ⊢ ◡ ∅ = { ⟨ 𝑧 , 𝑦 ⟩ ∣ 𝑦 ∅ 𝑧 } | |
| 6 | df-opab | ⊢ { ⟨ 𝑧 , 𝑦 ⟩ ∣ 𝑦 ∅ 𝑧 } = { 𝑥 ∣ ∃ 𝑧 ∃ 𝑦 ( 𝑥 = ⟨ 𝑧 , 𝑦 ⟩ ∧ 𝑦 ∅ 𝑧 ) } | |
| 7 | 5 6 | eqtri | ⊢ ◡ ∅ = { 𝑥 ∣ ∃ 𝑧 ∃ 𝑦 ( 𝑥 = ⟨ 𝑧 , 𝑦 ⟩ ∧ 𝑦 ∅ 𝑧 ) } |
| 8 | 7 | eqabri | ⊢ ( 𝑥 ∈ ◡ ∅ ↔ ∃ 𝑧 ∃ 𝑦 ( 𝑥 = ⟨ 𝑧 , 𝑦 ⟩ ∧ 𝑦 ∅ 𝑧 ) ) |
| 9 | 4 8 | mtbir | ⊢ ¬ 𝑥 ∈ ◡ ∅ |
| 10 | 9 | nel0 | ⊢ ◡ ∅ = ∅ |