Theorem eleq2d 2308

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 105   = wceq 1402   ∈ wcel 2209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is used by:  eleq12d  2309  eleqtrd  2317  neleqtrd  2336  neleqtrrd  2337  abeq2d  2351  eqabrd  2378  nfceqdf  2391  drnfc1  2409  drnfc2  2410  sbcbid  3109  cbvcsbw  3151  cbvcsb  3152  sbcel1g  3166  csbeq2d  3172  csbie2g  3198  cbvralcsf  3210  cbvrexcsf  3211  cbvreucsf  3212  cbvrabcsf  3213  rabsnif  3778  opeq1  3904  opeq2  3905  cbviun  4049  cbviin  4050  iinxsng  4086  iinxprg  4087  iunxsng  4088  iunxsngf  4090  cbvdisj  4116  disjnim  4120  disjiun  4125  mpteq12f  4211  axpweq  4308  rabxfrd  4615  onsucelsucexmid  4677  ordsucunielexmid  4678  0elsucexmid  4712  0nelelxp  4803  opeliunxp  4830  opeliunxp2  4920  iunxpf  4928  elrelimasn  5153  elimasng  5155  xpimasn  5236  ressn  5328  funfni  5483  fnbr  5485  fun11iun  5660  relndmfv  5728  fvelrnb  5750  foelcdmi  5755  fvun1  5769  fvco2  5774  elfvmptrab1  5801  elfvmptrab  5802  elpreima  5828  dff3im  5853  resflem  5872  fmptco  5874  funfvima3  5952  foima2  5957  eluniimadm  5971  dff13  5974  f1eqcocnv  5997  isoini  6024  riotaeqdv  6039  mpoeq123dva  6149  cbvmpox  6166  ovelrn  6238  elovmpod  6287  elovmpo  6288  elovmporab  6289  elovmporab1w  6290  fmpox  6436  disjxp1  6472  elsuppfng  6482  elsuppfn  6483  suppfnss  6497  suppcofn  6506  opeliunxp2f  6509  mpoxopn0yelv  6510  mpoxopovel  6512  rbropapd  6513  rntpos  6528  smoel  6571  smoiso  6573  smoel2  6574  tfrlem9  6590  tfrlemisucaccv  6596  tfrlemiubacc  6601  tfrlemi14d  6604  tfri2d  6607  tfr1onlemubacc  6617  tfr1onlemres  6620  tfrcllemubacc  6630  tfrcllemres  6633  rdgon  6657  freceq1  6663  freceq2  6664  frec0g  6668  frecabcl  6670  freccllem  6673  frecfcllem  6675  frecsuclem  6677  frecsuc  6678  nnsucelsuc  6764  nnsucuniel  6768  nnmordi  6789  ereldm  6852  iinerm  6881  elmapg  6935  elpmg  6938  elixpsn  7017  ixpsnf1o  7018  pw2f1odclem  7134  phplem4  7156  phplem3g  7157  phplem4on  7169  exmidpw  7215  fiintim  7238  fidcenumlemrks  7270  fidcenumlemrk  7271  elfi  7305  2omap  7318  ordiso2  7375  ctssdccl  7451  nnnninfeq  7468  cc2lem  7632  cc2  7633  cc3  7634  archnqq  7784  ltdfpr  7873  genpelxp  7878  genpelvl  7879  genpelvu  7880  addcanprleml  7981  addcanprlemu  7982  cauappcvgprlem1  8026  suplocexprlemell  8080  suplocexprlemmu  8085  suplocexprlemru  8086  suplocexprlemdisj  8087  suplocexprlemloc  8088  suplocexprlemub  8090  suplocexprlemlub  8091  cnm  8199  indval0  9299  eluz1  9934  elixx1  10309  elioo2  10333  elfz1  10426  elfzp1  10489  fzpr  10494  fzsuc2  10496  fzrev3  10504  elfzp12  10516  fzm1  10517  fzoval  10565  elfzo  10566  fzodcel  10570  elfzom1b  10657  fzosplitsni  10664  nninfdcex  10682  zmodidfzo  10803  frecuzrdgtcl  10862  frecuzrdgfunlem  10869  seqf1og  10971  bcval  11201  bcpasc  11218  hashf1lem1  11299  fundm2domnop0  11314  wrdmap  11350  elovmpowrd  11360  ccatfvalfi  11374  elfzelfzccat  11382  ccatlid  11388  ccatass  11390  ccatrn  11391  ccatalpha  11395  swrdfv2  11449  ccatswrd  11456  swrdccat2  11457  pfxfv  11470  pfxeq  11482  ccatpfx  11487  swrdswrd  11491  swrdpfx  11493  pfxpfx  11494  cats1un  11507  swrdccatfn  11510  swrdccatin1  11511  pfxccatin12lem4  11512  pfxccatin12lem1  11514  swrdccatin2  11515  pfxccatin12lem2c  11516  pfxccatin12lem2  11517  swrdccat3blem  11525  swrdccatin1d  11529  swrdccatin2d  11530  pfxccatin12d  11531  shftfn  11603  shftval  11604  seq3shft  11617  iser3shft  12128  sumeq1  12137  summodclem3  12163  summodclem2a  12164  isumss  12174  fsumsplit  12190  sumsplitdc  12215  fsum2dlemstep  12217  fisumcom2  12221  fsumparts  12253  explecnv  12288  fprodsplitdc  12379  fprodsplit  12380  fprod2dlemstep  12405  fprodcom2fi  12409  eftlub  12473  divalgmod  12710  bitsval  12726  bitsp1e  12735  bitsp1o  12736  algfx  12846  eucalgcvga  12852  reumodprminv  13052  nnnn0modprm0  13054  prmlem0  13240  ballotfilemfc0  13281  ballotfilemfcc  13282  ballotfilemsima  13308  ballotfilemrv  13312  ennnfonelemex  13354  ennnfonelemhom  13355  ennnfonelemf1  13358  ennnfonelemrn  13359  ctinfomlemom  13367  ctinfom  13368  ctiunctlemudc  13377  ctiunctlemf  13378  elrest  13649  ptex  13667  imasaddfnlemg  13684  divsfval  13698  xpscf  13717  grpidvalg  13742  grpidpropdg  13743  grpidd  13752  issgrpd  13776  sgrppropd  13777  ismndd  13799  mndpropd  13802  imasmnd2  13808  imasmnd  13809  ismhm  13817  issubm  13828  imasgrp2  13962  imasgrp  13963  issubg  14025  subginv  14033  isnsg  14054  eqg0el  14081  quselbasg  14082  isghm  14095  resghm2b  14114  conjnmzb  14132  conjnsg  14133  ghmpropd  14135  imasabl  14189  gzsumsplit0  14197  prdsbasmpt  14229  prdsbasmpt2  14237  pwselbasb  14255  mgpplusg  14271  mgpbas  14274  isrngd  14301  rngpropd  14303  imasrng  14304  qusrng  14306  rng1zrlem  14307  ringidval  14314  dfur2g  14315  srgidmlem  14331  issrgid  14334  ringcl  14366  isringid  14379  isringd  14395  imasring  14418  oppr0g  14436  oppr1g  14437  dvdsrvald  14449  isunitd  14462  unitinvcl  14479  unitinvinv  14480  unitlinv  14482  unitrinv  14483  unitnegcl  14486  dvdsrpropdg  14503  isrhm  14514  isrim0  14517  rhmmul  14520  islring  14548  opprlring  14553  issubrng  14556  opprsubrngg  14568  issubrg  14578  resrhm2b  14606  rhmpropd  14611  rrgval  14619  aprval  14640  aprap  14647  aprprop  14650  islmod  14676  lmodprop2d  14734  islssm  14743  islssmg  14744  islssmd  14745  lssats2  14800  ellspsn  14803  ixpsnbasval  14852  islidlm  14865  isridlrng  14868  rspssp  14880  rnglidlmmgm  14882  2idlval  14888  isridl  14890  2idlelb  14891  quscrng  14919  rspsn  14920  zrhval  15001  zrhrhmb  15006  znf1o  15035  asclfval  15070  assamulgscmlem2  15091  psrgrp  15125  mplelbascoe  15132  istopon  15163  eltg  15202  eltg2  15203  eltop  15219  eltop2  15220  eltop3  15221  iscld  15253  neiss2  15292  isnei  15294  lmfval  15343  cnfval  15344  iscn  15347  iscnp  15349  tgcn  15358  tgcnp  15359  lmbrf  15365  cnptopresti  15388  txbas  15408  eltx  15409  txdis  15427  txdis1cn  15428  hmeofvalg  15453  ishmeo  15454  ispsmet  15473  ismet  15494  isxmet  15495  elblps  15540  elbl  15541  elmopn  15596  neibl  15641  metrest  15656  txmetcnp  15668  txmetcn  15669  metcnpd  15670  elcncf  15723  ellimc3apf  15810  limcmpted  15813  cnlimcim  15821  cnlimc  15822  eldvap  15832  dvidsslem  15843  dviaddf  15855  dvimulf  15856  elply  15884  ply1termlem  15892  lgseisenlem3  16289  edgval  16399  edgiedgbg  16404  edgupgren  16480  upgredg  16483  uhgr2edg  16545  umgr2edg1  16548  usgredg2vlem1  16561  usgredg2vlem2  16562  ushgredgedg  16565  ushgredgedgloop  16567  subgruhgredgdm  16609  uhgrspansubgrlem  16615  vtxdgfval  16627  vtxedgfi  16628  vtxdgop  16631  vtxdg0v  16633  vtxdeqd  16635  vtxdfifiun  16636  1loopgrvd0fi  16645  1hevtxdg0fi  16646  1hevtxdg1en  16647  wksfval  16661  iswlk  16662  wlkm  16678  uspgr2wlkeq  16704  wlkreslem  16717  wlkres  16718  istrl  16724  clwwlkg  16732  isclwwlk  16733  clwwlkccatlem  16739  isclwwlkng  16745  clwwlkn0  16747  clwwlknnn  16751  clwwlkext2edg  16761  clwwlknonmpo  16767  clwwlknon  16768  clwwlk0on0  16770  iseupth  16786  eupth2lem3lem3fi  16809  eupth2lem3lem6fi  16810  eupth2lem3lem4fi  16812  eupth2lembfi  16816  bj-sels  17038  pw1map  17123  wexmiddiffilem  17141  wexmiddifxylem  17143  nninfall  17150  nninfsellemeq  17155