Theorem eqeq2d 1529

Description: Deduction from equality to equivalence of equalities.

Hypothesis

Ref	Expression
eqeq2d.1	⊢ (φ → A = B)

Assertion

Ref	Expression
eqeq2d	⊢ (φ → (C = A ↔ C = B))

Proof of Theorem eqeq2d

Step	Hyp	Ref	Expression
1		eqeq2d.1	. 2 ⊢ (φ → A = B)
2		eqeq2 1527	. 2 ⊢ (A = B → (C = A ↔ C = B))
3	1, 2	syl 10	1 ⊢ (φ → (C = A ↔ C = B))

Syntax hints:   → wi 3   ↔ wb 144   = wceq 992

This theorem is referenced by:  eqeq12d 1532  eqtrd 1550  eq2tri 1576  sbceq1dig 2065  eusn 2507  cbvopab 2746  cbvopab1 2748  cbvopab1s 2749  cbvopab2v 2751  opthg 2864  eqvinop 2867  moop2 2878  opabid 2887  dfid3 2914  limeq 2987  reusn 3115  reusni 3116  onsucuni2 3188  onuninsuci 3194  elvvv 3314  relop 3365  elxp4 3585  elxp5 3586  funopg 3652  funcnvuni 3669  iunfopab 3719  dffn5 3869  ssimaex 3879  fvopab4g 3890  fvopabn 3897  fvopab6 3905  fopabap 3955  fconst5 3962  abrexexlem1 3972  abrexexlem2 3973  abrexex 3974  dff13f 3989  f1fveq 3990  f1ocnvfv 3994  f1ocnvfvb 3995  rcla4eopr 4048  dfoprab2 4050  cbvoprab1 4057  cbvoprab12 4058  fnoprv 4077  oprabval2gf 4086  oprabval3 4090  oprabval4g 4091  oprabval4gALT 4092  oprabval6g 4093  fnrnoprv 4097  fooprv 4098  oprvex 4102  caoprcan 4116  fo1st 4152  fo2nd 4153  dfoprab4s 4176  dfoprab5sf 4178  df1st2 4188  df2nd2 4189  fsplit 4204  onopriun 4211  tz7.44-2 4230  tz7.44-3 4231  rdgeq1 4235  rdgeq2 4236  rdglem2 4239  tz7.48lem 4256  omv 4287  oev 4289  oe1m 4315  oarec 4332  nneob 4395  qseq2 4429  ecelqsi 4432  snec 4437  ecoptocl 4444  eceqopreq 4454  th3qlem1 4455  th3qlem2 4456  th3q 4458  en1 4567  mapsnen 4570  xpsnen 4576  xpassen 4582  pw2en 4587  ac6sfilem1 4588  mapxpen 4642  xpmapenlem3 4645  xpmapenlem4 4646  xpmapenlem5 4647  mapunen 4649  unfilem3 4696  abfii2 4705  abfii3 4706  abfii4 4707  pwfilem 4713  tz9.12lem1 4805  tz9.12lem3 4807  rankr1g 4821  rankuni 4844  aceq3lem 4878  aceq5lem1 4881  aceq5lem4 4884  aceq6b 4888  kmlem9 4919  unidom 4954  oncard 4976  cardsn 4982  cardalephex 5036  cf0 5060  cflecard 5062  cfsuc 5065  indpi 5188  genpv 5256  genpprecl 5258  genpass 5266  distrlem1pr 5281  distrlem5pr 5285  1idpr 5287  axcnre 5440  addcan 5506  subeq0 5557  neg11 5563  mulcant2i 5843  divmul3 5861  div11 5904  diveq0 5907  rec11i 5917  negeq0 5946  infm3lem 6221  nn0ind-raph 6385  zq 6399  qnegcl 6409  dfioo2 6530  icoshftf1oii 6536  icoshftf1olem 6537  fzen 6622  seq1lem1 6674  seq1val 6677  seq1suclem 6681  shftfval 6707  2shfti 6717  limsupval 6724  expge0 6785  expge1 6787  sq11 6826  sqeqor 6846  nn0opth2 6869  sqrmsq2i 6907  sqr2irrlem2 6926  sqr2irrlem3 6927  sqr2irrlem5 6929  crui 6938  cru 6939  creur 6943  creui 6944  replim 6962  abssubne0 7085  abs1mi 7107  sumeq2 7188  cbvsumi 7189  serzfsum 7207  fsumsplit 7223  serzclim0 7312  climaddc2 7322  climmulc2 7332  infcvgaux1i 7423  infcvgaux2i 7424  geolim 7442  geolim1 7444  divccncf 7485  efseq1ex 7511  eftlex 7583  ef1tlubi 7587  ef01tlubi 7591  absef01tlubi 7593  eirr 7599  ef4p 7608  reef11 7617  acdc3 7698  acdc2 7702  acdc5 7705  acdc 7707  nn0ennn 7709  ruclem12 7733  eltopsp 7816  tpsex 7817  istps 7818  tgval3 7837  subbas 7856  subbas2 7857  subtop 7858  ntrfval 7877  clsfval 7878  neifval 7924  lpfval 7952  islp2 7957  qdensere 7961  cnpfval 7967  blfval 8045  blrn3 8057  blelrn 8058  metdnsconst 8112  metcn4i 8183  xplm 8186  opr1cn 8189  opr2cn 8190  opr1scn 8191  fsumcnlem 8200  bcth 8243  isgrp 8254  grpid 8282  grpinvfval 8283  grpinvf 8297  grpdivfval 8299  gxoprval 8313  grplactfval 8337  grplactf1o 8339  vci 8414  isvclem 8443  isnvlem 8476  nvi 8480  nvmfval 8511  nvdm 8536  cnnvm 8560  vacnlem6 8587  vacn 8588  ipfval 8606  ip1cnilem4 8630  ip1cnilem5 8631  ip1cnilem6 8632  lnoval 8667  nmofval 8679  nmoval 8680  nmosetn0 8682  nmolb 8688  nmo0 8706  nmlno0lem 8708  nmlno0 8710  lnon0 8713  ajfval 8724  ipasslem6 8751  ipasslem11 8756  siilem2 8768  ajmoi 8775  minvecex 8838  htthlem3 8884  htthlem5 8886  spwval2 8915  spwval 8921  cosh111 8989  efghgrpilem 8991  efifolem1 8994  efifolem2 8995  efifolem3 8996  efifolem6 8999  efifo 9001  efif1lem6 9007  eff1i 9016  effoi 9017  hvaddcan 9212  hire 9236  hilnormi 9306  projlem8 9469  projlem10 9471  projlem15 9476  pjtheui 9511  pjmval 9514  pjeq2 9517  omlsii 9521  pjtheu2i 9526  pjpj0i 9531  axpjpj 9532  shsel3 9555  shscom 9559  dfchsup2 9574  dfchj2 9600  dfchj3 9601  h1de2ctlem 9754  elspansn 9765  elspansn2 9766  spansncol 9767  spanunsni 9778  h1datom 9781  hosmval 9787  hommval 9788  hodmval 9789  hfsmval 9790  hfmmval 9791  cmbr 9803  osumlem5 9860  spansncvi 9875  spansncv 9876  pjrni 9925  pj11 9937  pjpyth 9948  ho01i 10034  adjmo 10038  eigre 10041  eigorth 10044  nmopval 10062  nmopsetn0 10072  nmfnval 10083  nmfnsetn0 10085  eigvalval 10103  nmoplb 10111  nmfnlb 10128  adj1 10137  adjeq 10139  adjvalval 10141  braval 10147  bra0 10154  brafnmul 10155  kbval 10156  kbmul 10159  nmopnegi 10168  nmop0 10189  nmfn0 10190  nmlnop0iALT 10199  lnopeq 10213  nmopun 10218  lnopconi 10242  lnfnconi 10269  riesz3i 10274  riesz4i 10275  cnlnadjlem5 10283  cnlnadjlem9 10287  cnlnadji 10288  cnlnssadj 10292  nmopadjlei 10300  branmfn 10317  branmfnOLD 10318  rnbra 10320  cnvbraval 10323  kbass2 10330  kbass5 10333  elpjrnch 10399  atom1d 10561  superpos 10562  sumdmdlem 10627  cdjreui 10641  cdj3lem2 10644  cdj3lem3 10647  cdj3lem3b 10649  elghomlem1 10667  ghomf1olem 10681  cayleylem2 10695  infi1 10735  fine 10736  abfi 10737  ficli 10756  islatalg 10831  cur1val 10846  infi 10854  dupos1 10876  on1el3 10962  on1el4 10963  vri 10981  bsi 10995  hmeogrp 11044  subsp 11056  issubsplem1 11058  subspemp 11060  sbtpsines 11062  cnfilca 11088  rcfpfillem3 11091  rcfpfillem4 11092  rcfpfillem5 11093  rcfpfillem6 11094  sfvlim 11100  limfillem1 11101  fintopcomp 11115  bwt2 11123  trran 11159  trnij 11160  cnvtr 11161  isded 11190  dedi 11191  cmppfd 11199  domcmpd 11200  codcmpd 11201  iscat 11208  cati 11209  cmpasso 11227  ishoma 11242  ismonb 11265  ismonb2 11267  cmpmon 11270  isepib 11275  isepib2 11277  cinvlem1 11282  idfisf 11295  idsubfun 11312  subtr 11395  fiuni 11420  elfiun 11421  fictblem 11422  fictb 11423  inficlALT 11424  ordtypelem5 11431  ordtype 11434  hartoglem 11435  hartog 11436  omsubsuc 11438  omsublim 11448  opncldf1 11454  opncldf2 11455  opncldf3 11456  opnregcld 11467  cldregopn 11468  elsubsp 11477  subspid 11478  subsubtop 11479  subcld 11480  subcls 11481  compcov 11486  compsublem 11487  compsub 11488  uncomp 11490  hscptsscld 11491  compfipin0lem 11492  compfipin0 11493  cncomp 11494  alexsublem1 11496  alexsublem2 11497  alexsublem3 11498  alexsublem4 11499  alexsub 11500  subtopmet 11506  2ndcctbss 11539  isfne 11541  isfne3 11543  isref 11549  topfneec 11562  islocfin 11567  comppfsc 11578  neibastop2lem1 11580  neibastop2lem2 11581  neibastop2lem3 11582  neibastop2lem4 11583  neibastop3 11585  topmtcl 11586  topmeet 11587  topjoin 11588  fnemeet1 11589  fnemeet2 11590  fnejoin1 11591  fnejoin2 11592  fbasfip 11627  fsubbas 11630  fbunfip 11631  filrn 11643  isufil2 11650  ufilmax 11653  filssufillem 11655  filssufil 11656  ufileu 11658  fixufil 11661  limfil 11675  limfilcf 11683  flimcls 11684  hausfillim 11685  cnpfillim 11686  filmapf 11688  isfilmap 11689  elfilmap 11690  elfilmap3 11692  rnelfmlem 11698  rnelfm 11699  fmfnfmlem3 11702  fmfnfmlem4 11703  fmfnfm 11704  filfm 11706  flimff 11707  sflimf 11708  sfcls 11716  filclus 11717  fclusbas 11722  fcluscf 11724  fclsfnflim 11726  flimfnfcls 11727  fcluscnplem 11729  fcluscnp 11730  fcluscomp 11733  ufcomp 11734  fclusff 11735  sfclusf 11736  tailf 11756  istail 11757  filnetlem1 11763  filnetlem2 11764  filnetlem3 11765  filnetlem4 11766  filnetlem5 11767  filnet 11768  gapmlem 11783  opabex3 11806  oprabopabf 11807  oprabco 11811  cnvcan 11814  upxp 11822  upixp 11823  erthdmg 11824  dif1card 11835  fimax 11837  inficl 11849  sdc 11877  iserzshft2 11892  subspopn 11900  subspcld 11901  subspabs 11903  neificl 11904  metsstop 11909  icoopnst 11940  iocopnst 11941  cnres 11950  cnss 11953  piececn 11955  txbas 11973  txuni 11975  tx1cn 11976  tx2cn 11977  uptx 11978  txcn 11979  2txcn 11982  txsubsp 11983  txopn 11984  istotbnd 11989  sstotbnd 11992  totbndss 11993  isbnd3 11997  bndss 11998  blbnd 11999  totbndbnd 12000  ismtyval 12003  isismty 12004  ismtyhmeolem 12006  ismtybndlem 12008  heiborlem1 12011  heiborlem9 12019  heiborlem23 12033  heiborlem25 12035  heiborlem26 12036  heiborlem42 12052  rrnval 12069  rrntotbndlem1 12076  rrntotbnd 12078  iccbnd 12082  phtpyfval 12088  phtpyval 12089  phtpycom 12092  phtpycolem3 12095  phtpycolem4 12096  isphtpc 12101

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 999  ax-17 1007  ax-4 1009  ax-5o 1011  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-an 223  df-cleq 1511

Copyright terms: Public domain