MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cnv0 Structured version   Visualization version   GIF version

Theorem cnv0 5437
Description: The converse of the empty set. (Contributed by NM, 6-Apr-1998.)
Assertion
Ref Expression
cnv0 ∅ = ∅

Proof of Theorem cnv0
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 relcnv 5405 . 2 Rel
2 rel0 5151 . 2 Rel ∅
3 vex 3171 . . . 4 𝑥 ∈ V
4 vex 3171 . . . 4 𝑦 ∈ V
53, 4opelcnv 5210 . . 3 (⟨𝑥, 𝑦⟩ ∈ ∅ ↔ ⟨𝑦, 𝑥⟩ ∈ ∅)
6 noel 3873 . . . 4 ¬ ⟨𝑥, 𝑦⟩ ∈ ∅
7 noel 3873 . . . 4 ¬ ⟨𝑦, 𝑥⟩ ∈ ∅
86, 72false 363 . . 3 (⟨𝑥, 𝑦⟩ ∈ ∅ ↔ ⟨𝑦, 𝑥⟩ ∈ ∅)
95, 8bitr4i 265 . 2 (⟨𝑥, 𝑦⟩ ∈ ∅ ↔ ⟨𝑥, 𝑦⟩ ∈ ∅)
101, 2, 9eqrelriiv 5122 1 ∅ = ∅
Colors of variables: wff setvar class
Syntax hints:   = wceq 1474  wcel 1975  c0 3869  cop 4126  ccnv 5023
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-9 1984  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585  ax-sep 4699  ax-nul 4708  ax-pr 4824
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-eu 2457  df-mo 2458  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-ral 2896  df-rex 2897  df-rab 2900  df-v 3170  df-dif 3538  df-un 3540  df-in 3542  df-ss 3549  df-nul 3870  df-if 4032  df-sn 4121  df-pr 4123  df-op 4127  df-br 4574  df-opab 4634  df-xp 5030  df-rel 5031  df-cnv 5032
This theorem is referenced by:  xp0  5453  cnveq0  5491  co01  5549  funcnv0  5851  f10  6062  f1o00  6064  tpos0  7242  oduleval  16896  ust0  21771  nghmfval  22264  isnghm  22265  1pthonlem1  25881  mthmval  30528  resnonrel  36716  cononrel1  36718  cononrel2  36719  cnvrcl0  36750  0cnf  38562  mbf0  38649  1pthdlem1  41300
  Copyright terms: Public domain W3C validator