|   | 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 5295, ax-nul 5305, ax-pr 5431. (Revised by KP, 25-Oct-2021.) | 
| Ref | Expression | 
|---|---|
| cnv0 | ⊢ ◡∅ = ∅ | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | br0 5191 | . . . . . 6 ⊢ ¬ 𝑦∅𝑧 | |
| 2 | 1 | intnan 486 | . . . . 5 ⊢ ¬ (𝑥 = 〈𝑧, 𝑦〉 ∧ 𝑦∅𝑧) | 
| 3 | 2 | nex 1799 | . . . 4 ⊢ ¬ ∃𝑦(𝑥 = 〈𝑧, 𝑦〉 ∧ 𝑦∅𝑧) | 
| 4 | 3 | nex 1799 | . . 3 ⊢ ¬ ∃𝑧∃𝑦(𝑥 = 〈𝑧, 𝑦〉 ∧ 𝑦∅𝑧) | 
| 5 | df-cnv 5692 | . . . . 5 ⊢ ◡∅ = {〈𝑧, 𝑦〉 ∣ 𝑦∅𝑧} | |
| 6 | df-opab 5205 | . . . . 5 ⊢ {〈𝑧, 𝑦〉 ∣ 𝑦∅𝑧} = {𝑥 ∣ ∃𝑧∃𝑦(𝑥 = 〈𝑧, 𝑦〉 ∧ 𝑦∅𝑧)} | |
| 7 | 5, 6 | eqtri 2764 | . . . 4 ⊢ ◡∅ = {𝑥 ∣ ∃𝑧∃𝑦(𝑥 = 〈𝑧, 𝑦〉 ∧ 𝑦∅𝑧)} | 
| 8 | 7 | eqabri 2884 | . . 3 ⊢ (𝑥 ∈ ◡∅ ↔ ∃𝑧∃𝑦(𝑥 = 〈𝑧, 𝑦〉 ∧ 𝑦∅𝑧)) | 
| 9 | 4, 8 | mtbir 323 | . 2 ⊢ ¬ 𝑥 ∈ ◡∅ | 
| 10 | 9 | nel0 4353 | 1 ⊢ ◡∅ = ∅ | 
| Colors of variables: wff setvar class | 
| Syntax hints: ∧ wa 395 = wceq 1539 ∃wex 1778 ∈ wcel 2107 {cab 2713 ∅c0 4332 〈cop 4631 class class class wbr 5142 {copab 5204 ◡ccnv 5683 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-12 2176 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1542 df-fal 1552 df-ex 1779 df-sb 2064 df-clab 2714 df-cleq 2728 df-clel 2815 df-dif 3953 df-nul 4333 df-br 5143 df-opab 5205 df-cnv 5692 | 
| This theorem is referenced by: xp0 6177 cnveq0 6216 co01 6280 funcnv0 6631 f1o00 6882 tpos0 8282 cnvfi 9217 oduleval 18335 ust0 24229 nghmfval 24744 isnghm 24745 1pthdlem1 30155 mptiffisupp 32703 tocycf 33138 tocyc01 33139 mthmval 35581 resnonrel 43610 cononrel1 43612 cononrel2 43613 cnvrcl0 43643 0cnf 45897 | 
| Copyright terms: Public domain | W3C validator |