Theorem eleq2d 2302

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

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

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 2214

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

This theorem is referenced by:  eleq12d  2303  eleqtrd  2311  neleqtrd  2330  neleqtrrd  2331  abeq2d  2345  eqabrd  2370  nfceqdf  2383  drnfc1  2401  drnfc2  2402  sbcbid  3100  cbvcsbw  3142  cbvcsb  3143  sbcel1g  3157  csbeq2d  3163  csbie2g  3189  cbvralcsf  3201  cbvrexcsf  3202  cbvreucsf  3203  cbvrabcsf  3204  rabsnif  3758  opeq1  3883  opeq2  3884  cbviun  4028  cbviin  4029  iinxsng  4065  iinxprg  4066  iunxsng  4067  iunxsngf  4069  cbvdisj  4095  disjnim  4099  disjiun  4104  mpteq12f  4190  axpweq  4284  rabxfrd  4590  onsucelsucexmid  4652  ordsucunielexmid  4653  0elsucexmid  4687  0nelelxp  4778  opeliunxp  4805  opeliunxp2  4895  iunxpf  4903  elrelimasn  5128  elimasng  5130  xpimasn  5211  ressn  5303  funfni  5458  fnbr  5460  fun11iun  5635  fvelrnb  5724  foelcdmi  5729  fvun1  5743  fvco2  5746  elfvmptrab1  5772  elfvmptrab  5773  elpreima  5797  dff3im  5822  resflem  5841  fmptco  5843  funfvima3  5920  foima2  5924  eluniimadm  5938  dff13  5941  f1eqcocnv  5964  isoini  5991  riotaeqdv  6004  mpoeq123dva  6114  cbvmpox  6131  ovelrn  6203  elovmpod  6252  elovmpo  6253  elovmporab  6254  elovmporab1w  6255  fmpox  6396  disjxp1  6432  elsuppfng  6442  elsuppfn  6443  suppfnss  6457  suppcofn  6466  opeliunxp2f  6469  mpoxopn0yelv  6470  mpoxopovel  6472  rbropapd  6473  rntpos  6488  smoel  6531  smoiso  6533  smoel2  6534  tfrlem9  6550  tfrlemisucaccv  6556  tfrlemiubacc  6561  tfrlemi14d  6564  tfri2d  6567  tfr1onlemubacc  6577  tfr1onlemres  6580  tfrcllemubacc  6590  tfrcllemres  6593  rdgon  6617  freceq1  6623  freceq2  6624  frec0g  6628  frecabcl  6630  freccllem  6633  frecfcllem  6635  frecsuclem  6637  frecsuc  6638  nnsucelsuc  6724  nnsucuniel  6728  nnmordi  6749  ereldm  6812  iinerm  6841  elmapg  6895  elpmg  6898  elixpsn  6970  ixpsnf1o  6971  pw2f1odclem  7087  phplem4  7109  phplem3g  7110  phplem4on  7122  exmidpw  7168  fiintim  7191  fidcenumlemrks  7223  fidcenumlemrk  7224  elfi  7258  2omap  7269  ordiso2  7326  ctssdccl  7402  nnnninfeq  7419  cc2lem  7580  cc2  7581  cc3  7582  archnqq  7732  ltdfpr  7821  genpelxp  7826  genpelvl  7827  genpelvu  7828  addcanprleml  7929  addcanprlemu  7930  cauappcvgprlem1  7974  suplocexprlemell  8028  suplocexprlemmu  8033  suplocexprlemru  8034  suplocexprlemdisj  8035  suplocexprlemloc  8036  suplocexprlemub  8038  suplocexprlemlub  8039  cnm  8147  eluz1  9857  elixx1  10230  elioo2  10254  elfz1  10347  elfzp1  10406  fzpr  10411  fzsuc2  10413  fzrev3  10421  elfzp12  10433  fzm1  10434  fzoval  10482  elfzo  10483  fzodcel  10487  elfzom1b  10574  fzosplitsni  10581  nninfdcex  10597  zmodidfzo  10715  frecuzrdgtcl  10774  frecuzrdgfunlem  10781  seqf1og  10883  bcval  11111  bcpasc  11128  fundm2domnop0  11220  wrdmap  11256  elovmpowrd  11266  ccatfvalfi  11280  elfzelfzccat  11288  ccatlid  11294  ccatass  11296  ccatrn  11297  ccatalpha  11301  swrdfv2  11355  ccatswrd  11362  swrdccat2  11363  pfxfv  11376  pfxeq  11388  ccatpfx  11393  swrdswrd  11397  swrdpfx  11399  pfxpfx  11400  cats1un  11413  swrdccatfn  11416  swrdccatin1  11417  pfxccatin12lem4  11418  pfxccatin12lem1  11420  swrdccatin2  11421  pfxccatin12lem2c  11422  pfxccatin12lem2  11423  swrdccat3blem  11431  swrdccatin1d  11435  swrdccatin2d  11436  pfxccatin12d  11437  shftfn  11509  shftval  11510  seq3shft  11523  iser3shft  12031  sumeq1  12040  summodclem3  12066  summodclem2a  12067  isumss  12077  fsumsplit  12093  sumsplitdc  12118  fsum2dlemstep  12120  fisumcom2  12124  fsumparts  12156  explecnv  12191  fprodsplitdc  12282  fprodsplit  12283  fprod2dlemstep  12308  fprodcom2fi  12312  eftlub  12376  divalgmod  12613  bitsval  12629  bitsp1e  12638  bitsp1o  12639  algfx  12749  eucalgcvga  12755  reumodprminv  12951  nnnn0modprm0  12953  ennnfonelemex  13165  ennnfonelemhom  13166  ennnfonelemf1  13169  ennnfonelemrn  13170  ctinfomlemom  13178  ctinfom  13179  ctiunctlemudc  13188  ctiunctlemf  13189  elrest  13459  ptex  13477  prdsbasmpt  13493  prdsbasmpt2  13501  pwselbasb  13506  imasaddfnlemg  13527  divsfval  13541  xpscf  13560  grpidvalg  13586  grpidpropdg  13587  grpidd  13596  issgrpd  13625  sgrppropd  13626  ismndd  13650  mndpropd  13653  imasmnd2  13665  imasmnd  13666  ismhm  13674  issubm  13685  imasgrp2  13827  imasgrp  13828  issubg  13890  subginv  13898  isnsg  13919  eqg0el  13946  quselbasg  13947  isghm  13960  resghm2b  13979  conjnmzb  13997  conjnsg  13998  ghmpropd  14000  imasabl  14053  gsumsplit0  14063  isrngd  14097  rngpropd  14099  imasrng  14100  qusrng  14102  dfur2g  14106  srgidmlem  14122  issrgid  14125  ringcl  14157  isringid  14169  isringd  14185  imasring  14208  oppr0g  14225  oppr1g  14226  dvdsrvald  14238  isunitd  14251  unitinvcl  14268  unitinvinv  14269  unitlinv  14271  unitrinv  14272  unitnegcl  14275  dvdsrpropdg  14292  isrhm  14303  isrim0  14306  rhmmul  14309  islring  14337  issubrng  14344  opprsubrngg  14356  issubrg  14366  resrhm2b  14394  rhmpropd  14399  rrgval  14407  aprval  14428  aprap  14432  islmod  14439  lmodprop2d  14496  islssm  14505  islssmg  14506  islssmd  14507  lssats2  14562  ellspsn  14565  ixpsnbasval  14614  islidlm  14627  isridlrng  14630  rspssp  14642  rnglidlmmgm  14644  2idlval  14650  isridl  14652  2idlelb  14653  quscrng  14681  rspsn  14682  zrhval  14765  zrhrhmb  14770  znf1o  14799  psrgrp  14840  mplelbascoe  14847  istopon  14878  eltg  14917  eltg2  14918  eltop  14934  eltop2  14935  eltop3  14936  iscld  14968  neiss2  15007  isnei  15009  lmfval  15058  cnfval  15059  iscn  15062  iscnp  15064  tgcn  15073  tgcnp  15074  lmbrf  15080  cnptopresti  15103  txbas  15123  eltx  15124  txdis  15142  txdis1cn  15143  hmeofvalg  15168  ishmeo  15169  ispsmet  15188  ismet  15209  isxmet  15210  elblps  15255  elbl  15256  elmopn  15311  neibl  15356  metrest  15371  txmetcnp  15383  txmetcn  15384  metcnpd  15385  elcncf  15438  ellimc3apf  15525  limcmpted  15528  cnlimcim  15536  cnlimc  15537  eldvap  15547  dvidsslem  15558  dviaddf  15570  dvimulf  15571  elply  15599  ply1termlem  15607  lgseisenlem3  15945  edgval  16055  edgiedgbg  16060  edgupgren  16136  upgredg  16139  uhgr2edg  16201  umgr2edg1  16204  usgredg2vlem1  16217  usgredg2vlem2  16218  ushgredgedg  16221  ushgredgedgloop  16223  subgruhgredgdm  16265  uhgrspansubgrlem  16271  vtxdgfval  16283  vtxedgfi  16284  vtxdgop  16287  vtxdg0v  16289  vtxdeqd  16291  vtxdfifiun  16292  1loopgrvd0fi  16301  1hevtxdg0fi  16302  1hevtxdg1en  16303  wksfval  16317  iswlk  16318  wlkm  16334  uspgr2wlkeq  16360  wlkreslem  16373  wlkres  16374  istrl  16380  clwwlkg  16388  isclwwlk  16389  clwwlkccatlem  16395  isclwwlkng  16401  clwwlkn0  16403  clwwlknnn  16407  clwwlkext2edg  16417  clwwlknonmpo  16423  clwwlknon  16424  clwwlk0on0  16426  iseupth  16442  eupth2lem3lem3fi  16465  eupth2lem3lem6fi  16466  eupth2lem3lem4fi  16468  eupth2lembfi  16472  bj-sels  16684  pw1map  16769  nninfall  16787  nninfsellemeq  16792