Theorem eleq2d 2299

Description: Deduction from equality to equivalence of membership. (Contributed by NM, 27-Dec-1993.)

Hypothesis

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

Assertion

Ref	Expression
eleq2d	⊢ (𝜑 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵))

Proof of Theorem eleq2d

Step	Hyp	Ref	Expression
1		eleq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		eleq2 2293	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵))

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1395   ∈ wcel 2200

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-clel 2225

This theorem is referenced by:  eleq12d  2300  eleqtrd  2308  neleqtrd  2327  neleqtrrd  2328  abeq2d  2342  nfceqdf  2371  drnfc1  2389  drnfc2  2390  sbcbid  3087  cbvcsbw  3129  cbvcsb  3130  sbcel1g  3144  csbeq2d  3150  csbie2g  3176  cbvralcsf  3188  cbvrexcsf  3189  cbvreucsf  3190  cbvrabcsf  3191  rabsnif  3736  opeq1  3860  opeq2  3861  cbviun  4005  cbviin  4006  iinxsng  4042  iinxprg  4043  iunxsng  4044  iunxsngf  4046  cbvdisj  4072  disjnim  4076  disjiun  4081  mpteq12f  4167  axpweq  4259  rabxfrd  4564  onsucelsucexmid  4626  ordsucunielexmid  4627  0elsucexmid  4661  0nelelxp  4752  opeliunxp  4779  opeliunxp2  4868  iunxpf  4876  elrelimasn  5100  elimasng  5102  xpimasn  5183  ressn  5275  funfni  5429  fnbr  5431  fun11iun  5601  fvelrnb  5689  foelcdmi  5694  fvun1  5708  fvco2  5711  elfvmptrab1  5737  elfvmptrab  5738  elpreima  5762  dff3im  5788  resflem  5807  fmptco  5809  funfvima3  5883  foima2  5887  eluniimadm  5901  dff13  5904  f1eqcocnv  5927  isoini  5954  riotaeqdv  5967  mpoeq123dva  6077  cbvmpox  6094  ovelrn  6166  elovmpod  6215  elovmpo  6216  elovmporab  6217  elovmporab1w  6218  fmpox  6360  disjxp1  6396  opeliunxp2f  6399  mpoxopn0yelv  6400  mpoxopovel  6402  rbropapd  6403  rntpos  6418  smoel  6461  smoiso  6463  smoel2  6464  tfrlem9  6480  tfrlemisucaccv  6486  tfrlemiubacc  6491  tfrlemi14d  6494  tfri2d  6497  tfr1onlemubacc  6507  tfr1onlemres  6510  tfrcllemubacc  6520  tfrcllemres  6523  rdgon  6547  freceq1  6553  freceq2  6554  frec0g  6558  frecabcl  6560  freccllem  6563  frecfcllem  6565  frecsuclem  6567  frecsuc  6568  nnsucelsuc  6654  nnsucuniel  6658  nnmordi  6679  ereldm  6742  iinerm  6771  elmapg  6825  elpmg  6828  elixpsn  6899  ixpsnf1o  6900  pw2f1odclem  7015  phplem4  7036  phplem3g  7037  phplem4on  7049  exmidpw  7093  fiintim  7116  fidcenumlemrks  7143  fidcenumlemrk  7144  elfi  7161  ordiso2  7225  ctssdccl  7301  nnnninfeq  7318  cc2lem  7475  cc2  7476  cc3  7477  archnqq  7627  ltdfpr  7716  genpelxp  7721  genpelvl  7722  genpelvu  7723  addcanprleml  7824  addcanprlemu  7825  cauappcvgprlem1  7869  suplocexprlemell  7923  suplocexprlemmu  7928  suplocexprlemru  7929  suplocexprlemdisj  7930  suplocexprlemloc  7931  suplocexprlemub  7933  suplocexprlemlub  7934  cnm  8042  eluz1  9749  elixx1  10122  elioo2  10146  elfz1  10238  elfzp1  10297  fzpr  10302  fzsuc2  10304  fzrev3  10312  elfzp12  10324  fzm1  10325  fzoval  10373  elfzo  10374  fzodcel  10378  elfzom1b  10464  fzosplitsni  10471  nninfdcex  10487  zmodidfzo  10605  frecuzrdgtcl  10664  frecuzrdgfunlem  10671  seqf1og  10773  bcval  11001  bcpasc  11018  fundm2domnop0  11099  wrdmap  11135  elovmpowrd  11145  ccatfvalfi  11159  elfzelfzccat  11167  ccatlid  11173  ccatass  11175  ccatrn  11176  ccatalpha  11180  swrdfv2  11234  ccatswrd  11241  swrdccat2  11242  pfxfv  11255  pfxeq  11267  ccatpfx  11272  swrdswrd  11276  swrdpfx  11278  pfxpfx  11279  cats1un  11292  swrdccatfn  11295  swrdccatin1  11296  pfxccatin12lem4  11297  pfxccatin12lem1  11299  swrdccatin2  11300  pfxccatin12lem2c  11301  pfxccatin12lem2  11302  swrdccat3blem  11310  swrdccatin1d  11314  swrdccatin2d  11315  pfxccatin12d  11316  shftfn  11375  shftval  11376  seq3shft  11389  iser3shft  11897  sumeq1  11906  summodclem3  11931  summodclem2a  11932  isumss  11942  fsumsplit  11958  sumsplitdc  11983  fsum2dlemstep  11985  fisumcom2  11989  fsumparts  12021  explecnv  12056  fprodsplitdc  12147  fprodsplit  12148  fprod2dlemstep  12173  fprodcom2fi  12177  eftlub  12241  divalgmod  12478  bitsval  12494  bitsp1e  12503  bitsp1o  12504  algfx  12614  eucalgcvga  12620  reumodprminv  12816  nnnn0modprm0  12818  ennnfonelemex  13025  ennnfonelemhom  13026  ennnfonelemf1  13029  ennnfonelemrn  13030  ctinfomlemom  13038  ctinfom  13039  ctiunctlemudc  13048  ctiunctlemf  13049  elrest  13319  ptex  13337  prdsbasmpt  13353  prdsbasmpt2  13361  pwselbasb  13366  imasaddfnlemg  13387  divsfval  13401  xpscf  13420  grpidvalg  13446  grpidpropdg  13447  grpidd  13456  issgrpd  13485  sgrppropd  13486  ismndd  13510  mndpropd  13513  imasmnd2  13525  imasmnd  13526  ismhm  13534  issubm  13545  imasgrp2  13687  imasgrp  13688  issubg  13750  subginv  13758  isnsg  13779  eqg0el  13806  quselbasg  13807  isghm  13820  resghm2b  13839  conjnmzb  13857  conjnsg  13858  ghmpropd  13860  imasabl  13913  isrngd  13956  rngpropd  13958  imasrng  13959  qusrng  13961  dfur2g  13965  srgidmlem  13981  issrgid  13984  ringcl  14016  isringid  14028  isringd  14044  imasring  14067  oppr0g  14084  oppr1g  14085  dvdsrvald  14097  isunitd  14110  unitinvcl  14127  unitinvinv  14128  unitlinv  14130  unitrinv  14131  unitnegcl  14134  dvdsrpropdg  14151  isrhm  14162  isrim0  14165  rhmmul  14168  islring  14196  issubrng  14203  opprsubrngg  14215  issubrg  14225  resrhm2b  14253  rhmpropd  14258  rrgval  14266  aprval  14286  aprap  14290  islmod  14295  lmodprop2d  14352  islssm  14361  islssmg  14362  islssmd  14363  lssats2  14418  ellspsn  14421  ixpsnbasval  14470  islidlm  14483  isridlrng  14486  rspssp  14498  rnglidlmmgm  14500  2idlval  14506  isridl  14508  2idlelb  14509  quscrng  14537  rspsn  14538  zrhval  14621  zrhrhmb  14626  znf1o  14655  psrgrp  14689  mplelbascoe  14696  istopon  14727  eltg  14766  eltg2  14767  eltop  14783  eltop2  14784  eltop3  14785  iscld  14817  neiss2  14856  isnei  14858  lmfval  14907  cnfval  14908  iscn  14911  iscnp  14913  tgcn  14922  tgcnp  14923  lmbrf  14929  cnptopresti  14952  txbas  14972  eltx  14973  txdis  14991  txdis1cn  14992  hmeofvalg  15017  ishmeo  15018  ispsmet  15037  ismet  15058  isxmet  15059  elblps  15104  elbl  15105  elmopn  15160  neibl  15205  metrest  15220  txmetcnp  15232  txmetcn  15233  metcnpd  15234  elcncf  15287  ellimc3apf  15374  limcmpted  15377  cnlimcim  15385  cnlimc  15386  eldvap  15396  dvidsslem  15407  dviaddf  15419  dvimulf  15420  elply  15448  ply1termlem  15456  lgseisenlem3  15791  edgval  15901  edgiedgbg  15906  edgupgren  15980  upgredg  15983  uhgr2edg  16045  umgr2edg1  16048  usgredg2vlem1  16061  usgredg2vlem2  16062  ushgredgedg  16065  ushgredgedgloop  16067  vtxdgfval  16094  vtxedgfi  16095  vtxdgop  16098  vtxdg0v  16100  vtxdeqd  16102  vtxdfifiun  16103  1loopgrvd0fi  16112  1hevtxdg0fi  16113  wksfval  16119  iswlk  16120  wlkm  16136  uspgr2wlkeq  16162  wlkreslem  16173  wlkres  16174  istrl  16180  clwwlkg  16188  isclwwlk  16189  clwwlkccatlem  16195  isclwwlkng  16201  clwwlkn0  16203  clwwlknnn  16207  clwwlkext2edg  16217  clwwlknonmpo  16223  clwwlknon  16224  clwwlk0on0  16226  iseupth  16242  bj-sels  16445  2omap  16530  pw1map  16532  nninfall  16547  nninfsellemeq  16552