Theorem eleq2d 2301

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 2295	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵))

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1398   ∈ wcel 2202

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-clel 2227

This theorem is referenced by:  eleq12d  2302  eleqtrd  2310  neleqtrd  2329  neleqtrrd  2330  abeq2d  2344  nfceqdf  2374  drnfc1  2392  drnfc2  2393  sbcbid  3090  cbvcsbw  3132  cbvcsb  3133  sbcel1g  3147  csbeq2d  3153  csbie2g  3179  cbvralcsf  3191  cbvrexcsf  3192  cbvreucsf  3193  cbvrabcsf  3194  rabsnif  3742  opeq1  3867  opeq2  3868  cbviun  4012  cbviin  4013  iinxsng  4049  iinxprg  4050  iunxsng  4051  iunxsngf  4053  cbvdisj  4079  disjnim  4083  disjiun  4088  mpteq12f  4174  axpweq  4267  rabxfrd  4572  onsucelsucexmid  4634  ordsucunielexmid  4635  0elsucexmid  4669  0nelelxp  4760  opeliunxp  4787  opeliunxp2  4876  iunxpf  4884  elrelimasn  5109  elimasng  5111  xpimasn  5192  ressn  5284  funfni  5439  fnbr  5441  fun11iun  5613  fvelrnb  5702  foelcdmi  5707  fvun1  5721  fvco2  5724  elfvmptrab1  5750  elfvmptrab  5751  elpreima  5775  dff3im  5800  resflem  5819  fmptco  5821  funfvima3  5898  foima2  5902  eluniimadm  5916  dff13  5919  f1eqcocnv  5942  isoini  5969  riotaeqdv  5982  mpoeq123dva  6092  cbvmpox  6109  ovelrn  6181  elovmpod  6230  elovmpo  6231  elovmporab  6232  elovmporab1w  6233  fmpox  6374  disjxp1  6410  elsuppfng  6420  elsuppfn  6421  suppfnss  6435  suppcofn  6444  opeliunxp2f  6447  mpoxopn0yelv  6448  mpoxopovel  6450  rbropapd  6451  rntpos  6466  smoel  6509  smoiso  6511  smoel2  6512  tfrlem9  6528  tfrlemisucaccv  6534  tfrlemiubacc  6539  tfrlemi14d  6542  tfri2d  6545  tfr1onlemubacc  6555  tfr1onlemres  6558  tfrcllemubacc  6568  tfrcllemres  6571  rdgon  6595  freceq1  6601  freceq2  6602  frec0g  6606  frecabcl  6608  freccllem  6611  frecfcllem  6613  frecsuclem  6615  frecsuc  6616  nnsucelsuc  6702  nnsucuniel  6706  nnmordi  6727  ereldm  6790  iinerm  6819  elmapg  6873  elpmg  6876  elixpsn  6947  ixpsnf1o  6948  pw2f1odclem  7063  phplem4  7084  phplem3g  7085  phplem4on  7097  exmidpw  7143  fiintim  7166  fidcenumlemrks  7195  fidcenumlemrk  7196  elfi  7213  ordiso2  7277  ctssdccl  7353  nnnninfeq  7370  cc2lem  7528  cc2  7529  cc3  7530  archnqq  7680  ltdfpr  7769  genpelxp  7774  genpelvl  7775  genpelvu  7776  addcanprleml  7877  addcanprlemu  7878  cauappcvgprlem1  7922  suplocexprlemell  7976  suplocexprlemmu  7981  suplocexprlemru  7982  suplocexprlemdisj  7983  suplocexprlemloc  7984  suplocexprlemub  7986  suplocexprlemlub  7987  cnm  8095  eluz1  9803  elixx1  10176  elioo2  10200  elfz1  10293  elfzp1  10352  fzpr  10357  fzsuc2  10359  fzrev3  10367  elfzp12  10379  fzm1  10380  fzoval  10428  elfzo  10429  fzodcel  10433  elfzom1b  10520  fzosplitsni  10527  nninfdcex  10543  zmodidfzo  10661  frecuzrdgtcl  10720  frecuzrdgfunlem  10727  seqf1og  10829  bcval  11057  bcpasc  11074  fundm2domnop0  11158  wrdmap  11194  elovmpowrd  11204  ccatfvalfi  11218  elfzelfzccat  11226  ccatlid  11232  ccatass  11234  ccatrn  11235  ccatalpha  11239  swrdfv2  11293  ccatswrd  11300  swrdccat2  11301  pfxfv  11314  pfxeq  11326  ccatpfx  11331  swrdswrd  11335  swrdpfx  11337  pfxpfx  11338  cats1un  11351  swrdccatfn  11354  swrdccatin1  11355  pfxccatin12lem4  11356  pfxccatin12lem1  11358  swrdccatin2  11359  pfxccatin12lem2c  11360  pfxccatin12lem2  11361  swrdccat3blem  11369  swrdccatin1d  11373  swrdccatin2d  11374  pfxccatin12d  11375  shftfn  11447  shftval  11448  seq3shft  11461  iser3shft  11969  sumeq1  11978  summodclem3  12004  summodclem2a  12005  isumss  12015  fsumsplit  12031  sumsplitdc  12056  fsum2dlemstep  12058  fisumcom2  12062  fsumparts  12094  explecnv  12129  fprodsplitdc  12220  fprodsplit  12221  fprod2dlemstep  12246  fprodcom2fi  12250  eftlub  12314  divalgmod  12551  bitsval  12567  bitsp1e  12576  bitsp1o  12577  algfx  12687  eucalgcvga  12693  reumodprminv  12889  nnnn0modprm0  12891  ennnfonelemex  13098  ennnfonelemhom  13099  ennnfonelemf1  13102  ennnfonelemrn  13103  ctinfomlemom  13111  ctinfom  13112  ctiunctlemudc  13121  ctiunctlemf  13122  elrest  13392  ptex  13410  prdsbasmpt  13426  prdsbasmpt2  13434  pwselbasb  13439  imasaddfnlemg  13460  divsfval  13474  xpscf  13493  grpidvalg  13519  grpidpropdg  13520  grpidd  13529  issgrpd  13558  sgrppropd  13559  ismndd  13583  mndpropd  13586  imasmnd2  13598  imasmnd  13599  ismhm  13607  issubm  13618  imasgrp2  13760  imasgrp  13761  issubg  13823  subginv  13831  isnsg  13852  eqg0el  13879  quselbasg  13880  isghm  13893  resghm2b  13912  conjnmzb  13930  conjnsg  13931  ghmpropd  13933  imasabl  13986  gsumsplit0  13996  isrngd  14030  rngpropd  14032  imasrng  14033  qusrng  14035  dfur2g  14039  srgidmlem  14055  issrgid  14058  ringcl  14090  isringid  14102  isringd  14118  imasring  14141  oppr0g  14158  oppr1g  14159  dvdsrvald  14171  isunitd  14184  unitinvcl  14201  unitinvinv  14202  unitlinv  14204  unitrinv  14205  unitnegcl  14208  dvdsrpropdg  14225  isrhm  14236  isrim0  14239  rhmmul  14242  islring  14270  issubrng  14277  opprsubrngg  14289  issubrg  14299  resrhm2b  14327  rhmpropd  14332  rrgval  14340  aprval  14361  aprap  14365  islmod  14370  lmodprop2d  14427  islssm  14436  islssmg  14437  islssmd  14438  lssats2  14493  ellspsn  14496  ixpsnbasval  14545  islidlm  14558  isridlrng  14561  rspssp  14573  rnglidlmmgm  14575  2idlval  14581  isridl  14583  2idlelb  14584  quscrng  14612  rspsn  14613  zrhval  14696  zrhrhmb  14701  znf1o  14730  psrgrp  14769  mplelbascoe  14776  istopon  14807  eltg  14846  eltg2  14847  eltop  14863  eltop2  14864  eltop3  14865  iscld  14897  neiss2  14936  isnei  14938  lmfval  14987  cnfval  14988  iscn  14991  iscnp  14993  tgcn  15002  tgcnp  15003  lmbrf  15009  cnptopresti  15032  txbas  15052  eltx  15053  txdis  15071  txdis1cn  15072  hmeofvalg  15097  ishmeo  15098  ispsmet  15117  ismet  15138  isxmet  15139  elblps  15184  elbl  15185  elmopn  15240  neibl  15285  metrest  15300  txmetcnp  15312  txmetcn  15313  metcnpd  15314  elcncf  15367  ellimc3apf  15454  limcmpted  15457  cnlimcim  15465  cnlimc  15466  eldvap  15476  dvidsslem  15487  dviaddf  15499  dvimulf  15500  elply  15528  ply1termlem  15536  lgseisenlem3  15874  edgval  15984  edgiedgbg  15989  edgupgren  16065  upgredg  16068  uhgr2edg  16130  umgr2edg1  16133  usgredg2vlem1  16146  usgredg2vlem2  16147  ushgredgedg  16150  ushgredgedgloop  16152  subgruhgredgdm  16194  uhgrspansubgrlem  16200  vtxdgfval  16212  vtxedgfi  16213  vtxdgop  16216  vtxdg0v  16218  vtxdeqd  16220  vtxdfifiun  16221  1loopgrvd0fi  16230  1hevtxdg0fi  16231  1hevtxdg1en  16232  wksfval  16246  iswlk  16247  wlkm  16263  uspgr2wlkeq  16289  wlkreslem  16302  wlkres  16303  istrl  16309  clwwlkg  16317  isclwwlk  16318  clwwlkccatlem  16324  isclwwlkng  16330  clwwlkn0  16332  clwwlknnn  16336  clwwlkext2edg  16346  clwwlknonmpo  16352  clwwlknon  16353  clwwlk0on0  16355  iseupth  16371  eupth2lem3lem3fi  16394  eupth2lem3lem6fi  16395  eupth2lem3lem4fi  16397  eupth2lembfi  16401  bj-sels  16613  2omap  16698  pw1map  16700  nninfall  16718  nninfsellemeq  16723