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  3086  cbvcsbw  3128  cbvcsb  3129  sbcel1g  3143  csbeq2d  3149  csbie2g  3175  cbvralcsf  3187  cbvrexcsf  3188  cbvreucsf  3189  cbvrabcsf  3190  opeq1  3857  opeq2  3858  cbviun  4002  cbviin  4003  iinxsng  4039  iinxprg  4040  iunxsng  4041  iunxsngf  4043  cbvdisj  4069  disjnim  4073  disjiun  4078  mpteq12f  4164  axpweq  4255  rabxfrd  4560  onsucelsucexmid  4622  ordsucunielexmid  4623  0elsucexmid  4657  0nelelxp  4748  opeliunxp  4774  opeliunxp2  4862  iunxpf  4870  elrelimasn  5094  elimasng  5096  xpimasn  5177  ressn  5269  funfni  5423  fnbr  5425  fun11iun  5595  fvelrnb  5683  foelcdmi  5688  fvun1  5702  fvco2  5705  elfvmptrab1  5731  elfvmptrab  5732  elpreima  5756  dff3im  5782  resflem  5801  fmptco  5803  funfvima3  5877  foima2  5881  eluniimadm  5895  dff13  5898  f1eqcocnv  5921  isoini  5948  riotaeqdv  5961  mpoeq123dva  6071  cbvmpox  6088  ovelrn  6160  elovmpod  6209  elovmpo  6210  elovmporab  6211  elovmporab1w  6212  fmpox  6352  disjxp1  6388  opeliunxp2f  6390  mpoxopn0yelv  6391  mpoxopovel  6393  rbropapd  6394  rntpos  6409  smoel  6452  smoiso  6454  smoel2  6455  tfrlem9  6471  tfrlemisucaccv  6477  tfrlemiubacc  6482  tfrlemi14d  6485  tfri2d  6488  tfr1onlemubacc  6498  tfr1onlemres  6501  tfrcllemubacc  6511  tfrcllemres  6514  rdgon  6538  freceq1  6544  freceq2  6545  frec0g  6549  frecabcl  6551  freccllem  6554  frecfcllem  6556  frecsuclem  6558  frecsuc  6559  nnsucelsuc  6645  nnsucuniel  6649  nnmordi  6670  ereldm  6733  iinerm  6762  elmapg  6816  elpmg  6819  elixpsn  6890  ixpsnf1o  6891  pw2f1odclem  7003  phplem4  7024  phplem3g  7025  phplem4on  7037  exmidpw  7081  fiintim  7104  fidcenumlemrks  7131  fidcenumlemrk  7132  elfi  7149  ordiso2  7213  ctssdccl  7289  nnnninfeq  7306  cc2lem  7463  cc2  7464  cc3  7465  archnqq  7615  ltdfpr  7704  genpelxp  7709  genpelvl  7710  genpelvu  7711  addcanprleml  7812  addcanprlemu  7813  cauappcvgprlem1  7857  suplocexprlemell  7911  suplocexprlemmu  7916  suplocexprlemru  7917  suplocexprlemdisj  7918  suplocexprlemloc  7919  suplocexprlemub  7921  suplocexprlemlub  7922  cnm  8030  eluz1  9737  elixx1  10105  elioo2  10129  elfz1  10221  elfzp1  10280  fzpr  10285  fzsuc2  10287  fzrev3  10295  elfzp12  10307  fzm1  10308  fzoval  10356  elfzo  10357  fzodcel  10361  elfzom1b  10447  fzosplitsni  10453  nninfdcex  10469  zmodidfzo  10587  frecuzrdgtcl  10646  frecuzrdgfunlem  10653  seqf1og  10755  bcval  10983  bcpasc  11000  fundm2domnop0  11080  wrdmap  11116  elovmpowrd  11126  ccatfvalfi  11140  elfzelfzccat  11148  ccatlid  11154  ccatass  11156  ccatrn  11157  ccatalpha  11161  swrdfv2  11210  ccatswrd  11217  swrdccat2  11218  pfxfv  11231  pfxeq  11243  ccatpfx  11248  swrdswrd  11252  swrdpfx  11254  pfxpfx  11255  cats1un  11268  swrdccatfn  11271  swrdccatin1  11272  pfxccatin12lem4  11273  pfxccatin12lem1  11275  swrdccatin2  11276  pfxccatin12lem2c  11277  pfxccatin12lem2  11278  swrdccat3blem  11286  swrdccatin1d  11290  swrdccatin2d  11291  pfxccatin12d  11292  shftfn  11350  shftval  11351  seq3shft  11364  iser3shft  11872  sumeq1  11881  summodclem3  11906  summodclem2a  11907  isumss  11917  fsumsplit  11933  sumsplitdc  11958  fsum2dlemstep  11960  fisumcom2  11964  fsumparts  11996  explecnv  12031  fprodsplitdc  12122  fprodsplit  12123  fprod2dlemstep  12148  fprodcom2fi  12152  eftlub  12216  divalgmod  12453  bitsval  12469  bitsp1e  12478  bitsp1o  12479  algfx  12589  eucalgcvga  12595  reumodprminv  12791  nnnn0modprm0  12793  ennnfonelemex  13000  ennnfonelemhom  13001  ennnfonelemf1  13004  ennnfonelemrn  13005  ctinfomlemom  13013  ctinfom  13014  ctiunctlemudc  13023  ctiunctlemf  13024  elrest  13294  ptex  13312  prdsbasmpt  13328  prdsbasmpt2  13336  pwselbasb  13341  imasaddfnlemg  13362  divsfval  13376  xpscf  13395  grpidvalg  13421  grpidpropdg  13422  grpidd  13431  issgrpd  13460  sgrppropd  13461  ismndd  13485  mndpropd  13488  imasmnd2  13500  imasmnd  13501  ismhm  13509  issubm  13520  imasgrp2  13662  imasgrp  13663  issubg  13725  subginv  13733  isnsg  13754  eqg0el  13781  quselbasg  13782  isghm  13795  resghm2b  13814  conjnmzb  13832  conjnsg  13833  ghmpropd  13835  imasabl  13888  isrngd  13931  rngpropd  13933  imasrng  13934  qusrng  13936  dfur2g  13940  srgidmlem  13956  issrgid  13959  ringcl  13991  isringid  14003  isringd  14019  imasring  14042  oppr0g  14059  oppr1g  14060  dvdsrvald  14072  isunitd  14085  unitinvcl  14102  unitinvinv  14103  unitlinv  14105  unitrinv  14106  unitnegcl  14109  dvdsrpropdg  14126  isrhm  14137  isrim0  14140  rhmmul  14143  islring  14171  issubrng  14178  opprsubrngg  14190  issubrg  14200  resrhm2b  14228  rhmpropd  14233  rrgval  14241  aprval  14261  aprap  14265  islmod  14270  lmodprop2d  14327  islssm  14336  islssmg  14337  islssmd  14338  lssats2  14393  ellspsn  14396  ixpsnbasval  14445  islidlm  14458  isridlrng  14461  rspssp  14473  rnglidlmmgm  14475  2idlval  14481  isridl  14483  2idlelb  14484  quscrng  14512  rspsn  14513  zrhval  14596  zrhrhmb  14601  znf1o  14630  psrgrp  14664  mplelbascoe  14671  istopon  14702  eltg  14741  eltg2  14742  eltop  14758  eltop2  14759  eltop3  14760  iscld  14792  neiss2  14831  isnei  14833  lmfval  14882  cnfval  14883  iscn  14886  iscnp  14888  tgcn  14897  tgcnp  14898  lmbrf  14904  cnptopresti  14927  txbas  14947  eltx  14948  txdis  14966  txdis1cn  14967  hmeofvalg  14992  ishmeo  14993  ispsmet  15012  ismet  15033  isxmet  15034  elblps  15079  elbl  15080  elmopn  15135  neibl  15180  metrest  15195  txmetcnp  15207  txmetcn  15208  metcnpd  15209  elcncf  15262  ellimc3apf  15349  limcmpted  15352  cnlimcim  15360  cnlimc  15361  eldvap  15371  dvidsslem  15382  dviaddf  15394  dvimulf  15395  elply  15423  ply1termlem  15431  lgseisenlem3  15766  edgiedgbg  15880  edgupgren  15954  upgredg  15957  uhgr2edg  16019  umgr2edg1  16022  usgredg2vlem1  16035  usgredg2vlem2  16036  ushgredgedg  16039  ushgredgedgloop  16041  vtxdgfval  16047  vtxedgfi  16048  vtxdgop  16051  vtxdg0v  16053  vtxdeqd  16055  vtxdfifiun  16056  wksfval  16063  iswlk  16064  wlkm  16080  uspgr2wlkeq  16106  wlkreslem  16117  wlkres  16118  istrl  16124  clwwlkg  16131  isclwwlk  16132  clwwlkccatlem  16137  bj-sels  16332  2omap  16418  pw1map  16420  nninfall  16435  nninfsellemeq  16440