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 ⊢ (𝜑 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵))

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1402   ∈ wcel 2209

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

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

This theorem is referenced 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  3774  opeq1  3899  opeq2  3900  cbviun  4044  cbviin  4045  iinxsng  4081  iinxprg  4082  iunxsng  4083  iunxsngf  4085  cbvdisj  4111  disjnim  4115  disjiun  4120  mpteq12f  4206  axpweq  4303  rabxfrd  4610  onsucelsucexmid  4672  ordsucunielexmid  4673  0elsucexmid  4707  0nelelxp  4798  opeliunxp  4825  opeliunxp2  4915  iunxpf  4923  elrelimasn  5148  elimasng  5150  xpimasn  5231  ressn  5323  funfni  5478  fnbr  5480  fun11iun  5655  fvelrnb  5744  foelcdmi  5749  fvun1  5763  fvco2  5768  elfvmptrab1  5794  elfvmptrab  5795  elpreima  5819  dff3im  5844  resflem  5863  fmptco  5865  funfvima3  5942  foima2  5947  eluniimadm  5961  dff13  5964  f1eqcocnv  5987  isoini  6014  riotaeqdv  6029  mpoeq123dva  6139  cbvmpox  6156  ovelrn  6228  elovmpod  6277  elovmpo  6278  elovmporab  6279  elovmporab1w  6280  fmpox  6426  disjxp1  6462  elsuppfng  6472  elsuppfn  6473  suppfnss  6487  suppcofn  6496  opeliunxp2f  6499  mpoxopn0yelv  6500  mpoxopovel  6502  rbropapd  6503  rntpos  6518  smoel  6561  smoiso  6563  smoel2  6564  tfrlem9  6580  tfrlemisucaccv  6586  tfrlemiubacc  6591  tfrlemi14d  6594  tfri2d  6597  tfr1onlemubacc  6607  tfr1onlemres  6610  tfrcllemubacc  6620  tfrcllemres  6623  rdgon  6647  freceq1  6653  freceq2  6654  frec0g  6658  frecabcl  6660  freccllem  6663  frecfcllem  6665  frecsuclem  6667  frecsuc  6668  nnsucelsuc  6754  nnsucuniel  6758  nnmordi  6779  ereldm  6842  iinerm  6871  elmapg  6925  elpmg  6928  elixpsn  7007  ixpsnf1o  7008  pw2f1odclem  7124  phplem4  7146  phplem3g  7147  phplem4on  7159  exmidpw  7205  fiintim  7228  fidcenumlemrks  7260  fidcenumlemrk  7261  elfi  7295  2omap  7308  ordiso2  7365  ctssdccl  7441  nnnninfeq  7458  cc2lem  7622  cc2  7623  cc3  7624  archnqq  7774  ltdfpr  7863  genpelxp  7868  genpelvl  7869  genpelvu  7870  addcanprleml  7971  addcanprlemu  7972  cauappcvgprlem1  8016  suplocexprlemell  8070  suplocexprlemmu  8075  suplocexprlemru  8076  suplocexprlemdisj  8077  suplocexprlemloc  8078  suplocexprlemub  8080  suplocexprlemlub  8081  cnm  8189  eluz1  9904  elixx1  10278  elioo2  10302  elfz1  10395  elfzp1  10457  fzpr  10462  fzsuc2  10464  fzrev3  10472  elfzp12  10484  fzm1  10485  fzoval  10533  elfzo  10534  fzodcel  10538  elfzom1b  10625  fzosplitsni  10632  nninfdcex  10650  zmodidfzo  10768  frecuzrdgtcl  10827  frecuzrdgfunlem  10834  seqf1og  10936  bcval  11165  bcpasc  11182  hashf1lem1  11263  fundm2domnop0  11278  wrdmap  11314  elovmpowrd  11324  ccatfvalfi  11338  elfzelfzccat  11346  ccatlid  11352  ccatass  11354  ccatrn  11355  ccatalpha  11359  swrdfv2  11413  ccatswrd  11420  swrdccat2  11421  pfxfv  11434  pfxeq  11446  ccatpfx  11451  swrdswrd  11455  swrdpfx  11457  pfxpfx  11458  cats1un  11471  swrdccatfn  11474  swrdccatin1  11475  pfxccatin12lem4  11476  pfxccatin12lem1  11478  swrdccatin2  11479  pfxccatin12lem2c  11480  pfxccatin12lem2  11481  swrdccat3blem  11489  swrdccatin1d  11493  swrdccatin2d  11494  pfxccatin12d  11495  shftfn  11567  shftval  11568  seq3shft  11581  iser3shft  12090  sumeq1  12099  summodclem3  12125  summodclem2a  12126  isumss  12136  fsumsplit  12152  sumsplitdc  12177  fsum2dlemstep  12179  fisumcom2  12183  fsumparts  12215  explecnv  12250  fprodsplitdc  12341  fprodsplit  12342  fprod2dlemstep  12367  fprodcom2fi  12371  eftlub  12435  divalgmod  12672  bitsval  12688  bitsp1e  12697  bitsp1o  12698  algfx  12808  eucalgcvga  12814  reumodprminv  13010  nnnn0modprm0  13012  ballotfilemfc0  13210  ballotfilemfcc  13211  ballotfilemsima  13237  ballotfilemrv  13241  ennnfonelemex  13283  ennnfonelemhom  13284  ennnfonelemf1  13287  ennnfonelemrn  13288  ctinfomlemom  13296  ctinfom  13297  ctiunctlemudc  13306  ctiunctlemf  13307  elrest  13577  ptex  13595  imasaddfnlemg  13612  divsfval  13626  xpscf  13645  grpidvalg  13670  grpidpropdg  13671  grpidd  13680  issgrpd  13704  sgrppropd  13705  ismndd  13727  mndpropd  13730  imasmnd2  13736  imasmnd  13737  ismhm  13745  issubm  13756  imasgrp2  13890  imasgrp  13891  issubg  13953  subginv  13961  isnsg  13982  eqg0el  14009  quselbasg  14010  isghm  14023  resghm2b  14042  conjnmzb  14060  conjnsg  14061  ghmpropd  14063  imasabl  14117  gzsumsplit0  14125  prdsbasmpt  14157  prdsbasmpt2  14165  pwselbasb  14183  isrngd  14227  rngpropd  14229  imasrng  14230  qusrng  14232  rng1zrlem  14233  dfur2g  14240  srgidmlem  14256  issrgid  14259  ringcl  14291  isringid  14303  isringd  14319  imasring  14342  oppr0g  14360  oppr1g  14361  dvdsrvald  14373  isunitd  14386  unitinvcl  14403  unitinvinv  14404  unitlinv  14406  unitrinv  14407  unitnegcl  14410  dvdsrpropdg  14427  isrhm  14438  isrim0  14441  rhmmul  14444  islring  14472  opprlring  14477  issubrng  14480  opprsubrngg  14492  issubrg  14502  resrhm2b  14530  rhmpropd  14535  rrgval  14543  aprval  14564  aprap  14571  aprprop  14574  islmod  14600  lmodprop2d  14657  islssm  14666  islssmg  14667  islssmd  14668  lssats2  14723  ellspsn  14726  ixpsnbasval  14775  islidlm  14788  isridlrng  14791  rspssp  14803  rnglidlmmgm  14805  2idlval  14811  isridl  14813  2idlelb  14814  quscrng  14842  rspsn  14843  zrhval  14924  zrhrhmb  14929  znf1o  14958  psrgrp  14999  mplelbascoe  15006  istopon  15037  eltg  15076  eltg2  15077  eltop  15093  eltop2  15094  eltop3  15095  iscld  15127  neiss2  15166  isnei  15168  lmfval  15217  cnfval  15218  iscn  15221  iscnp  15223  tgcn  15232  tgcnp  15233  lmbrf  15239  cnptopresti  15262  txbas  15282  eltx  15283  txdis  15301  txdis1cn  15302  hmeofvalg  15327  ishmeo  15328  ispsmet  15347  ismet  15368  isxmet  15369  elblps  15414  elbl  15415  elmopn  15470  neibl  15515  metrest  15530  txmetcnp  15542  txmetcn  15543  metcnpd  15544  elcncf  15597  ellimc3apf  15684  limcmpted  15687  cnlimcim  15695  cnlimc  15696  eldvap  15706  dvidsslem  15717  dviaddf  15729  dvimulf  15730  elply  15758  ply1termlem  15766  lgseisenlem3  16105  edgval  16215  edgiedgbg  16220  edgupgren  16296  upgredg  16299  uhgr2edg  16361  umgr2edg1  16364  usgredg2vlem1  16377  usgredg2vlem2  16378  ushgredgedg  16381  ushgredgedgloop  16383  subgruhgredgdm  16425  uhgrspansubgrlem  16431  vtxdgfval  16443  vtxedgfi  16444  vtxdgop  16447  vtxdg0v  16449  vtxdeqd  16451  vtxdfifiun  16452  1loopgrvd0fi  16461  1hevtxdg0fi  16462  1hevtxdg1en  16463  wksfval  16477  iswlk  16478  wlkm  16494  uspgr2wlkeq  16520  wlkreslem  16533  wlkres  16534  istrl  16540  clwwlkg  16548  isclwwlk  16549  clwwlkccatlem  16555  isclwwlkng  16561  clwwlkn0  16563  clwwlknnn  16567  clwwlkext2edg  16577  clwwlknonmpo  16583  clwwlknon  16584  clwwlk0on0  16586  iseupth  16602  eupth2lem3lem3fi  16625  eupth2lem3lem6fi  16626  eupth2lem3lem4fi  16628  eupth2lembfi  16632  bj-sels  16854  pw1map  16939  nninfall  16957  nninfsellemeq  16962