Theorem cnveqd 5749

Description: Equality deduction for converse relation. (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 5747	. 2 ⊢ (𝐴 = 𝐵 → ◡𝐴 = ◡𝐵)
3	1, 2	syl 17	1 ⊢ (𝜑 → ◡𝐴 = ◡𝐵)

Syntax hints:   → wi 4   = wceq 1536  ^◡ccnv 5557

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-in 3946  df-ss 3955  df-br 5070  df-opab 5132  df-cnv 5566

This theorem is referenced by:  opswap  6089  cores2  6115  fimacnvinrn  6843  nvocnv  7041  2ndval2  7710  2nd1st  7740  cnvf1olem  7808  fparlem3  7812  fparlem4  7813  brtpos2  7901  dftpos4  7914  tpostpos  7915  tposf12  7920  xpcomco  8610  infeq123d  8948  cantnffval2  9161  cnfcomlem  9165  fseqenlem2  9454  dfac12lem1  9572  dfac12r  9575  fpwwe2cbv  10055  fpwwe2lem2  10057  fpwwe2lem6  10060  fpwwe2lem9  10063  fpwwecbv  10069  fpwwelem  10070  funcnvs2  14278  funcnvs3  14279  funcnvs4  14280  relexpcnv  14397  fsumcnv  15131  fprodcnv  15340  bitsf1ocnv  15796  vdwpc  16319  imasval  16787  xpsval  16846  monfval  17005  ismon  17006  monpropd  17010  isepi  17013  invffval  17031  invfval  17032  dfiso2  17045  isofn  17048  oppcinv  17053  isfth  17187  catcisolem  17369  oduval  17743  oduleval  17744  gsumvalx  17889  grpinvcnv  18170  grplactcnv  18205  eqglact  18334  gsumcom2  19098  isunit  19410  issrng  19624  znval  20685  znle2  20703  evpmss  20733  psgnevpmb  20734  ptbasfi  22192  ptval2  22212  ptrescn  22250  xkoptsub  22265  qtopval  22306  txswaphmeolem  22415  ptcmpg  22668  tgplacthmeo  22714  trust  22841  prdsxmslem2  23142  metuval  23162  nghmfval  23334  isnghm  23335  pi1xfrcnv  23664  ismbf1  24228  ismbf  24232  mbfconst  24237  mbfres2  24249  cncombf  24262  deg1val  24693  fta1glem2  24763  fta1g  24764  fta1b  24766  dgrval  24821  dgrlem  24822  coe11  24846  fta1lem  24899  vieta1lem2  24903  ispth  27507  uhgrwkspthlem2  27538  usgr2wlkspthlem1  27541  usgr2wlkspthlem2  27542  pthdlem1  27550  2spthd  27723  3spthd  27958  f1o3d  30375  xppreima2  30398  ofpreima  30413  fcnvgreu  30421  fpwrelmapffslem  30471  tocycfv  30755  tocycf  30763  cycpm2tr  30765  cycpmconjvlem  30787  evpmval  30791  altgnsg  30795  ordtrest2NEW  31170  qqhval  31219  indf1ofs  31289  esum2dlem  31355  mbfmcst  31521  omssubadd  31562  sitgfval  31603  eulerpartlemgf  31641  orvcval  31719  pthhashvtx  32378  cvmliftmolem1  32532  cvmliftlem5  32540  cvmliftlem15  32549  cvmlift2lem9a  32554  cvmlift2lem9  32562  ismfs  32800  mthmval  32826  wsuceq123  33105  cnambfre  34944  itg2addnclem2  34948  ftc1anclem1  34971  ftc1anclem6  34976  dfsymrels2  35785  dfsymrel2  35789  cdlemg1finvtrlemN  37715  tendoicbv  37933  tendoi  37934  tendoi2  37935  tendoicl  37936  docaffvalN  38261  docafvalN  38262  dihmeetlem1N  38430  dihglblem5apreN  38431  diophrw  39362  rmxfval  39507  rmyfval  39508  aomclem8  39667  cnvtrclfv  40075  frege131d  40115  dssmapnvod  40372  smfpimioo  43069  smfpimcc  43089  smfsuplem2  43093