Theorem cnveqi 5182

Description: Equality inference for converse. (Contributed by NM, 23-Dec-2008.)

Hypothesis

Ref	Expression
cnveqi.1

Assertion

Ref	Expression
cnveqi

Proof of Theorem cnveqi

Step	Hyp	Ref	Expression
1		cnveqi.1	. 2
2		cnveq 5181	. 2
3	1, 2	ax-mp 5	1

Syntax hints:  =wceq 1395  `'ccnv 5003

This theorem is referenced by:  mptcnv  5413  cnvin  5418  cnvxp  5429  xp0  5430  imainrect  5453  cnvcnv  5464  mptpreima  5505  co01  5527  coi2  5529  fcoi1  5764  f1oprswap  5860  f1ocnvd  6524  fun11iun  6760  fparlem3  6902  fparlem4  6903  tz7.48-2  7126  mapsncnv  7485  sbthlem8  7654  1sdom  7742  infxpenc2  8420  infxpenc2OLD  8424  compsscnv  8772  zorn2lem4  8900  fsumcom2  13589  fprodcom2  13788  strlemor1  14724  xpsc  14954  fthoppc  15292  oduval  15760  oduleval  15761  dprdfidOLD  17064  pjdm  18738  qtopres  20199  xkocnv  20315  ustneism  20726  mbfres  22051  dflog2  22948  dfrelog  22953  dvlog  23032  efopnlem2  23038  axcontlem2  24268  0pth  24572  1pthonlem1  24591  constr2spthlem1  24596  2pthlem1  24597  constr3pthlem2  24656  ex-cnv  25158  cnvadj  26811  gtiso  27519  cnvoprab  27546  f1od2  27547  ordtcnvNEW  27902  ordtrest2NEW  27905  mbfmcst  28230  0rrv  28390  ballotlemrinv  28472  mthmpps  28942  pprodcnveq  29533  cytpval  31169  cnvtrrel  37782

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-in 3482  df-ss 3489  df-br 4453  df-opab 4511  df-cnv 5012