Theorem cnveqd 5220

Description: Equality deduction for converse. (Contributed by NM, 6-Dec-2013.)

Hypothesis

Ref	Expression
cnveqd.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
cnveqd	⊢ (𝜑 → ◡𝐴 = ◡𝐵)

Proof of Theorem cnveqd

Step	Hyp	Ref	Expression
1		cnveqd.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		cnveq 5218	. 2 ⊢ (𝐴 = 𝐵 → ◡𝐴 = ◡𝐵)
3	1, 2	syl 17	1 ⊢ (𝜑 → ◡𝐴 = ◡𝐵)

Syntax hints:   → wi 4   = wceq 1475  ^◡ccnv 5037

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-in 3547  df-ss 3554  df-br 4584  df-opab 4644  df-cnv 5046

This theorem is referenced by:  cnvsng  5539  opswap  5540  cores2  5565  fimacnvinrn  6256  nvocnv  6437  2ndval2  7077  2nd1st  7104  cnvf1olem  7162  fparlem3  7166  fparlem4  7167  brtpos2  7245  dftpos4  7258  tpostpos  7259  tposf12  7264  xpcomco  7935  infeq123d  8270  cantnffval2  8475  cnfcomlem  8479  fseqenlem2  8731  dfac12lem1  8848  dfac12r  8851  fpwwe2cbv  9331  fpwwe2lem2  9333  fpwwe2lem6  9336  fpwwe2lem9  9339  fpwwecbv  9345  fpwwelem  9346  funcnvs2  13508  funcnvs3  13509  funcnvs4  13510  relexpcnv  13623  fsumcnv  14346  fprodcnv  14552  bitsf1ocnv  15004  vdwpc  15522  imasval  15994  xpsfval  16050  xpsval  16055  monfval  16215  ismon  16216  monpropd  16220  isepi  16223  invffval  16241  invfval  16242  dfiso2  16255  isofn  16258  oppcinv  16263  isfth  16397  catcisolem  16579  oduval  16953  oduleval  16954  gsumvalx  17093  grpinvcnv  17306  grplactcnv  17341  eqglact  17468  gsumcom2  18197  isunit  18480  issrng  18673  znval  19702  znle2  19721  evpmss  19751  psgnevpmb  19752  ptbasfi  21194  ptval2  21214  ptrescn  21252  xkoptsub  21267  qtopval  21308  txswaphmeolem  21417  xpstopnlem2  21424  ptcmpg  21671  tgplacthmeo  21717  trust  21843  prdsxmslem2  22144  metuval  22164  nghmfval  22336  isnghm  22337  pi1xfrcnv  22665  ismbf1  23199  ismbf  23203  mbfconst  23208  mbfres2  23218  cncombf  23231  deg1val  23660  fta1glem2  23730  fta1g  23731  fta1b  23733  dgrval  23788  dgrlem  23789  coe11  23813  fta1lem  23866  vieta1lem2  23870  ispth  26098  1pthonlem1  26119  constr2spthlem1  26124  2pthlem1  26125  constr2pth  26131  constr3pthlem2  26184  f1o3d  28813  xppreima2  28830  ofpreima  28848  fcnvgreu  28855  fpwrelmapffslem  28895  ordtrest2NEW  29297  qqhval  29346  indf1ofs  29415  esum2dlem  29481  mbfmcst  29648  omssubadd  29689  sitgfval  29730  eulerpartlemgf  29768  orvcval  29846  cvmliftmolem1  30517  cvmliftlem5  30525  cvmliftlem15  30534  cvmlift2lem9a  30539  cvmlift2lem9  30547  ismfs  30700  mthmval  30726  wsuceq123  31004  cnambfre  32628  itg2addnclem2  32632  ftc1anclem1  32655  ftc1anclem6  32660  cdlemg1finvtrlemN  34881  tendoicbv  35099  tendoi  35100  tendoi2  35101  tendoicl  35102  docaffvalN  35428  docafvalN  35429  dihmeetlem1N  35597  dihglblem5apreN  35598  diophrw  36340  rmxfval  36486  rmyfval  36487  aomclem8  36649  cnvtrclfv  37035  frege131d  37075  dssmapnvod  37334  smfpimioo  39672  isPth  40929  uhgr1wlkspthlem2  40960  usgr2wlkspthlem1  40963  usgr2wlkspthlem2  40964  pthdlem1  40972  2spthd  41148  3spthd  41343