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 1397   ∈ 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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  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  2373  drnfc1  2391  drnfc2  2392  sbcbid  3089  cbvcsbw  3131  cbvcsb  3132  sbcel1g  3146  csbeq2d  3152  csbie2g  3178  cbvralcsf  3190  cbvrexcsf  3191  cbvreucsf  3192  cbvrabcsf  3193  rabsnif  3738  opeq1  3862  opeq2  3863  cbviun  4007  cbviin  4008  iinxsng  4044  iinxprg  4045  iunxsng  4046  iunxsngf  4048  cbvdisj  4074  disjnim  4078  disjiun  4083  mpteq12f  4169  axpweq  4261  rabxfrd  4566  onsucelsucexmid  4628  ordsucunielexmid  4629  0elsucexmid  4663  0nelelxp  4754  opeliunxp  4781  opeliunxp2  4870  iunxpf  4878  elrelimasn  5102  elimasng  5104  xpimasn  5185  ressn  5277  funfni  5432  fnbr  5434  fun11iun  5604  fvelrnb  5693  foelcdmi  5698  fvun1  5712  fvco2  5715  elfvmptrab1  5741  elfvmptrab  5742  elpreima  5766  dff3im  5792  resflem  5811  fmptco  5813  funfvima3  5888  foima2  5892  eluniimadm  5906  dff13  5909  f1eqcocnv  5932  isoini  5959  riotaeqdv  5972  mpoeq123dva  6082  cbvmpox  6099  ovelrn  6171  elovmpod  6220  elovmpo  6221  elovmporab  6222  elovmporab1w  6223  fmpox  6365  disjxp1  6401  opeliunxp2f  6404  mpoxopn0yelv  6405  mpoxopovel  6407  rbropapd  6408  rntpos  6423  smoel  6466  smoiso  6468  smoel2  6469  tfrlem9  6485  tfrlemisucaccv  6491  tfrlemiubacc  6496  tfrlemi14d  6499  tfri2d  6502  tfr1onlemubacc  6512  tfr1onlemres  6515  tfrcllemubacc  6525  tfrcllemres  6528  rdgon  6552  freceq1  6558  freceq2  6559  frec0g  6563  frecabcl  6565  freccllem  6568  frecfcllem  6570  frecsuclem  6572  frecsuc  6573  nnsucelsuc  6659  nnsucuniel  6663  nnmordi  6684  ereldm  6747  iinerm  6776  elmapg  6830  elpmg  6833  elixpsn  6904  ixpsnf1o  6905  pw2f1odclem  7020  phplem4  7041  phplem3g  7042  phplem4on  7054  exmidpw  7100  fiintim  7123  fidcenumlemrks  7152  fidcenumlemrk  7153  elfi  7170  ordiso2  7234  ctssdccl  7310  nnnninfeq  7327  cc2lem  7485  cc2  7486  cc3  7487  archnqq  7637  ltdfpr  7726  genpelxp  7731  genpelvl  7732  genpelvu  7733  addcanprleml  7834  addcanprlemu  7835  cauappcvgprlem1  7879  suplocexprlemell  7933  suplocexprlemmu  7938  suplocexprlemru  7939  suplocexprlemdisj  7940  suplocexprlemloc  7941  suplocexprlemub  7943  suplocexprlemlub  7944  cnm  8052  eluz1  9759  elixx1  10132  elioo2  10156  elfz1  10248  elfzp1  10307  fzpr  10312  fzsuc2  10314  fzrev3  10322  elfzp12  10334  fzm1  10335  fzoval  10383  elfzo  10384  fzodcel  10388  elfzom1b  10475  fzosplitsni  10482  nninfdcex  10498  zmodidfzo  10616  frecuzrdgtcl  10675  frecuzrdgfunlem  10682  seqf1og  10784  bcval  11012  bcpasc  11029  fundm2domnop0  11113  wrdmap  11149  elovmpowrd  11159  ccatfvalfi  11173  elfzelfzccat  11181  ccatlid  11187  ccatass  11189  ccatrn  11190  ccatalpha  11194  swrdfv2  11248  ccatswrd  11255  swrdccat2  11256  pfxfv  11269  pfxeq  11281  ccatpfx  11286  swrdswrd  11290  swrdpfx  11292  pfxpfx  11293  cats1un  11306  swrdccatfn  11309  swrdccatin1  11310  pfxccatin12lem4  11311  pfxccatin12lem1  11313  swrdccatin2  11314  pfxccatin12lem2c  11315  pfxccatin12lem2  11316  swrdccat3blem  11324  swrdccatin1d  11328  swrdccatin2d  11329  pfxccatin12d  11330  shftfn  11389  shftval  11390  seq3shft  11403  iser3shft  11911  sumeq1  11920  summodclem3  11946  summodclem2a  11947  isumss  11957  fsumsplit  11973  sumsplitdc  11998  fsum2dlemstep  12000  fisumcom2  12004  fsumparts  12036  explecnv  12071  fprodsplitdc  12162  fprodsplit  12163  fprod2dlemstep  12188  fprodcom2fi  12192  eftlub  12256  divalgmod  12493  bitsval  12509  bitsp1e  12518  bitsp1o  12519  algfx  12629  eucalgcvga  12635  reumodprminv  12831  nnnn0modprm0  12833  ennnfonelemex  13040  ennnfonelemhom  13041  ennnfonelemf1  13044  ennnfonelemrn  13045  ctinfomlemom  13053  ctinfom  13054  ctiunctlemudc  13063  ctiunctlemf  13064  elrest  13334  ptex  13352  prdsbasmpt  13368  prdsbasmpt2  13376  pwselbasb  13381  imasaddfnlemg  13402  divsfval  13416  xpscf  13435  grpidvalg  13461  grpidpropdg  13462  grpidd  13471  issgrpd  13500  sgrppropd  13501  ismndd  13525  mndpropd  13528  imasmnd2  13540  imasmnd  13541  ismhm  13549  issubm  13560  imasgrp2  13702  imasgrp  13703  issubg  13765  subginv  13773  isnsg  13794  eqg0el  13821  quselbasg  13822  isghm  13835  resghm2b  13854  conjnmzb  13872  conjnsg  13873  ghmpropd  13875  imasabl  13928  gsumsplit0  13938  isrngd  13972  rngpropd  13974  imasrng  13975  qusrng  13977  dfur2g  13981  srgidmlem  13997  issrgid  14000  ringcl  14032  isringid  14044  isringd  14060  imasring  14083  oppr0g  14100  oppr1g  14101  dvdsrvald  14113  isunitd  14126  unitinvcl  14143  unitinvinv  14144  unitlinv  14146  unitrinv  14147  unitnegcl  14150  dvdsrpropdg  14167  isrhm  14178  isrim0  14181  rhmmul  14184  islring  14212  issubrng  14219  opprsubrngg  14231  issubrg  14241  resrhm2b  14269  rhmpropd  14274  rrgval  14282  aprval  14302  aprap  14306  islmod  14311  lmodprop2d  14368  islssm  14377  islssmg  14378  islssmd  14379  lssats2  14434  ellspsn  14437  ixpsnbasval  14486  islidlm  14499  isridlrng  14502  rspssp  14514  rnglidlmmgm  14516  2idlval  14522  isridl  14524  2idlelb  14525  quscrng  14553  rspsn  14554  zrhval  14637  zrhrhmb  14642  znf1o  14671  psrgrp  14705  mplelbascoe  14712  istopon  14743  eltg  14782  eltg2  14783  eltop  14799  eltop2  14800  eltop3  14801  iscld  14833  neiss2  14872  isnei  14874  lmfval  14923  cnfval  14924  iscn  14927  iscnp  14929  tgcn  14938  tgcnp  14939  lmbrf  14945  cnptopresti  14968  txbas  14988  eltx  14989  txdis  15007  txdis1cn  15008  hmeofvalg  15033  ishmeo  15034  ispsmet  15053  ismet  15074  isxmet  15075  elblps  15120  elbl  15121  elmopn  15176  neibl  15221  metrest  15236  txmetcnp  15248  txmetcn  15249  metcnpd  15250  elcncf  15303  ellimc3apf  15390  limcmpted  15393  cnlimcim  15401  cnlimc  15402  eldvap  15412  dvidsslem  15423  dviaddf  15435  dvimulf  15436  elply  15464  ply1termlem  15472  lgseisenlem3  15807  edgval  15917  edgiedgbg  15922  edgupgren  15998  upgredg  16001  uhgr2edg  16063  umgr2edg1  16066  usgredg2vlem1  16079  usgredg2vlem2  16080  ushgredgedg  16083  ushgredgedgloop  16085  subgruhgredgdm  16127  uhgrspansubgrlem  16133  vtxdgfval  16145  vtxedgfi  16146  vtxdgop  16149  vtxdg0v  16151  vtxdeqd  16153  vtxdfifiun  16154  1loopgrvd0fi  16163  1hevtxdg0fi  16164  1hevtxdg1en  16165  wksfval  16179  iswlk  16180  wlkm  16196  uspgr2wlkeq  16222  wlkreslem  16235  wlkres  16236  istrl  16242  clwwlkg  16250  isclwwlk  16251  clwwlkccatlem  16257  isclwwlkng  16263  clwwlkn0  16265  clwwlknnn  16269  clwwlkext2edg  16279  clwwlknonmpo  16285  clwwlknon  16286  clwwlk0on0  16288  iseupth  16304  eupth2lem3lem3fi  16327  eupth2lem3lem6fi  16328  eupth2lem3lem4fi  16330  eupth2lembfi  16334  bj-sels  16535  2omap  16620  pw1map  16622  nninfall  16637  nninfsellemeq  16642