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 5194, ax-nul 5201, ax-pr 5320. (Revised by KP, 25-Oct-2021.) |
Ref | Expression |
---|---|
cnv0 | ⊢ ◡∅ = ∅ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | br0 5106 | . . . . . 6 ⊢ ¬ 𝑦∅𝑧 | |
2 | 1 | intnan 487 | . . . . 5 ⊢ ¬ (𝑥 = 〈𝑧, 𝑦〉 ∧ 𝑦∅𝑧) |
3 | 2 | nex 1792 | . . . 4 ⊢ ¬ ∃𝑦(𝑥 = 〈𝑧, 𝑦〉 ∧ 𝑦∅𝑧) |
4 | 3 | nex 1792 | . . 3 ⊢ ¬ ∃𝑧∃𝑦(𝑥 = 〈𝑧, 𝑦〉 ∧ 𝑦∅𝑧) |
5 | df-cnv 5556 | . . . . 5 ⊢ ◡∅ = {〈𝑧, 𝑦〉 ∣ 𝑦∅𝑧} | |
6 | df-opab 5120 | . . . . 5 ⊢ {〈𝑧, 𝑦〉 ∣ 𝑦∅𝑧} = {𝑥 ∣ ∃𝑧∃𝑦(𝑥 = 〈𝑧, 𝑦〉 ∧ 𝑦∅𝑧)} | |
7 | 5, 6 | eqtri 2841 | . . . 4 ⊢ ◡∅ = {𝑥 ∣ ∃𝑧∃𝑦(𝑥 = 〈𝑧, 𝑦〉 ∧ 𝑦∅𝑧)} |
8 | 7 | abeq2i 2945 | . . 3 ⊢ (𝑥 ∈ ◡∅ ↔ ∃𝑧∃𝑦(𝑥 = 〈𝑧, 𝑦〉 ∧ 𝑦∅𝑧)) |
9 | 4, 8 | mtbir 324 | . 2 ⊢ ¬ 𝑥 ∈ ◡∅ |
10 | 9 | nel0 4308 | 1 ⊢ ◡∅ = ∅ |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 396 = wceq 1528 ∃wex 1771 ∈ wcel 2105 {cab 2796 ∅c0 4288 〈cop 4563 class class class wbr 5057 {copab 5119 ◡ccnv 5547 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-dif 3936 df-nul 4289 df-br 5058 df-opab 5120 df-cnv 5556 |
This theorem is referenced by: xp0 6008 cnveq0 6047 co01 6107 funcnv0 6413 f1o00 6642 tpos0 7911 oduleval 17729 ust0 22755 nghmfval 23258 isnghm 23259 1pthdlem1 27841 tocycf 30686 tocyc01 30687 mthmval 32719 resnonrel 39830 cononrel1 39832 cononrel2 39833 cnvrcl0 39863 0cnf 42036 |
Copyright terms: Public domain | W3C validator |