Theorem cnv0 5535

Description: The converse of the empty set. (Contributed by NM, 6-Apr-1998.) Remove dependency on ax-sep 4781, ax-nul 4789, ax-pr 4906. (Revised by KP, 25-Oct-2021.)

Assertion

Ref	Expression
cnv0	|- `' (/) = (/)

Proof of Theorem cnv0

Dummy variables x y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		br0 4701	. . . . . 6 |- -. y (/) z
2	1	intnan 960	. . . . 5 |- -. ( x = <. z , y >. /\ y (/) z )
3	2	nex 1731	. . . 4 |- -. E. y ( x = <. z , y >. /\ y (/) z )
4	3	nex 1731	. . 3 |- -. E. z E. y ( x = <. z , y >. /\ y (/) z )
5		df-cnv 5122	. . . . 5 |- `' (/) = { <. z , y >. | y (/) z }
6		df-opab 4713	. . . . 5 |- { <. z , y >. | y (/) z } = { x | E. z E. y ( x = <. z , y >. /\ y (/) z ) }
7	5, 6	eqtri 2644	. . . 4 |- `' (/) = { x | E. z E. y ( x = <. z , y >. /\ y (/) z ) }
8	7	abeq2i 2735	. . 3 |- ( x e. `' (/) <-> E. z E. y ( x = <. z , y >. /\ y (/) z ) )
9	4, 8	mtbir 313	. 2 |- -. x e. `' (/)
10	9	nel0 3932	1 |- `' (/) = (/)

Syntax hints:   /\ wa 384   = wceq 1483   E.wex 1704   e. wcel 1990   {cab 2608   (/)c0 3915   <.cop 4183   class class class wbr 4653   {copab 4712   `'ccnv 5113

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-dif 3577  df-nul 3916  df-br 4654  df-opab 4713  df-cnv 5122

This theorem is referenced by:  xp0  5552  cnveq0  5591  co01  5650  funcnv0  5955  f10  6169  f1o00  6171  tpos0  7382  oduleval  17131  ust0  22023  nghmfval  22526  isnghm  22527  1pthdlem1  26995  mthmval  31472  resnonrel  37898  cononrel1  37900  cononrel2  37901  cnvrcl0  37932  0cnf  40090  mbf0  40173