![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > cnv0 | Structured version Visualization version GIF version |
Description: The converse of the empty set. (Contributed by NM, 6-Apr-1998.) Remove dependency on ax-sep 5300, ax-nul 5307, ax-pr 5428. (Revised by KP, 25-Oct-2021.) |
Ref | Expression |
---|---|
cnv0 | ⊢ ◡∅ = ∅ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | br0 5198 | . . . . . 6 ⊢ ¬ 𝑦∅𝑧 | |
2 | 1 | intnan 488 | . . . . 5 ⊢ ¬ (𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦∅𝑧) |
3 | 2 | nex 1803 | . . . 4 ⊢ ¬ ∃𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦∅𝑧) |
4 | 3 | nex 1803 | . . 3 ⊢ ¬ ∃𝑧∃𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦∅𝑧) |
5 | df-cnv 5685 | . . . . 5 ⊢ ◡∅ = {⟨𝑧, 𝑦⟩ ∣ 𝑦∅𝑧} | |
6 | df-opab 5212 | . . . . 5 ⊢ {⟨𝑧, 𝑦⟩ ∣ 𝑦∅𝑧} = {𝑥 ∣ ∃𝑧∃𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦∅𝑧)} | |
7 | 5, 6 | eqtri 2761 | . . . 4 ⊢ ◡∅ = {𝑥 ∣ ∃𝑧∃𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦∅𝑧)} |
8 | 7 | eqabri 2878 | . . 3 ⊢ (𝑥 ∈ ◡∅ ↔ ∃𝑧∃𝑦(𝑥 = ⟨𝑧, 𝑦⟩ ∧ 𝑦∅𝑧)) |
9 | 4, 8 | mtbir 323 | . 2 ⊢ ¬ 𝑥 ∈ ◡∅ |
10 | 9 | nel0 4351 | 1 ⊢ ◡∅ = ∅ |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 397 = wceq 1542 ∃wex 1782 ∈ wcel 2107 {cab 2710 ∅c0 4323 ⟨cop 4635 class class class wbr 5149 {copab 5211 ◡ccnv 5676 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-12 2172 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-dif 3952 df-nul 4324 df-br 5150 df-opab 5212 df-cnv 5685 |
This theorem is referenced by: xp0 6158 cnveq0 6197 co01 6261 funcnv0 6615 f1o00 6869 tpos0 8241 cnvfi 9180 oduleval 18242 ust0 23724 nghmfval 24239 isnghm 24240 1pthdlem1 29388 mptiffisupp 31915 tocycf 32276 tocyc01 32277 mthmval 34566 resnonrel 42343 cononrel1 42345 cononrel2 42346 cnvrcl0 42376 0cnf 44593 |
Copyright terms: Public domain | W3C validator |