Theorem eleq2d 2304

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

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

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 2216

This theorem depends on definitions:  df-bi 117  df-cleq 2227  df-clel 2230

This theorem is referenced by:  eleq12d  2305  eleqtrd  2313  neleqtrd  2332  neleqtrrd  2333  abeq2d  2347  eqabrd  2372  nfceqdf  2385  drnfc1  2403  drnfc2  2404  sbcbid  3103  cbvcsbw  3145  cbvcsb  3146  sbcel1g  3160  csbeq2d  3166  csbie2g  3192  cbvralcsf  3204  cbvrexcsf  3205  cbvreucsf  3206  cbvrabcsf  3207  rabsnif  3763  opeq1  3888  opeq2  3889  cbviun  4033  cbviin  4034  iinxsng  4070  iinxprg  4071  iunxsng  4072  iunxsngf  4074  cbvdisj  4100  disjnim  4104  disjiun  4109  mpteq12f  4195  axpweq  4289  rabxfrd  4595  onsucelsucexmid  4657  ordsucunielexmid  4658  0elsucexmid  4692  0nelelxp  4783  opeliunxp  4810  opeliunxp2  4900  iunxpf  4908  elrelimasn  5133  elimasng  5135  xpimasn  5216  ressn  5308  funfni  5463  fnbr  5465  fun11iun  5640  fvelrnb  5729  foelcdmi  5734  fvun1  5748  fvco2  5751  elfvmptrab1  5777  elfvmptrab  5778  elpreima  5802  dff3im  5827  resflem  5846  fmptco  5848  funfvima3  5925  foima2  5930  eluniimadm  5944  dff13  5947  f1eqcocnv  5970  isoini  5997  riotaeqdv  6012  mpoeq123dva  6122  cbvmpox  6139  ovelrn  6211  elovmpod  6260  elovmpo  6261  elovmporab  6262  elovmporab1w  6263  fmpox  6409  disjxp1  6445  elsuppfng  6455  elsuppfn  6456  suppfnss  6470  suppcofn  6479  opeliunxp2f  6482  mpoxopn0yelv  6483  mpoxopovel  6485  rbropapd  6486  rntpos  6501  smoel  6544  smoiso  6546  smoel2  6547  tfrlem9  6563  tfrlemisucaccv  6569  tfrlemiubacc  6574  tfrlemi14d  6577  tfri2d  6580  tfr1onlemubacc  6590  tfr1onlemres  6593  tfrcllemubacc  6603  tfrcllemres  6606  rdgon  6630  freceq1  6636  freceq2  6637  frec0g  6641  frecabcl  6643  freccllem  6646  frecfcllem  6648  frecsuclem  6650  frecsuc  6651  nnsucelsuc  6737  nnsucuniel  6741  nnmordi  6762  ereldm  6825  iinerm  6854  elmapg  6908  elpmg  6911  elixpsn  6983  ixpsnf1o  6984  pw2f1odclem  7100  phplem4  7122  phplem3g  7123  phplem4on  7135  exmidpw  7181  fiintim  7204  fidcenumlemrks  7236  fidcenumlemrk  7237  elfi  7271  2omap  7282  ordiso2  7339  ctssdccl  7415  nnnninfeq  7432  cc2lem  7596  cc2  7597  cc3  7598  archnqq  7748  ltdfpr  7837  genpelxp  7842  genpelvl  7843  genpelvu  7844  addcanprleml  7945  addcanprlemu  7946  cauappcvgprlem1  7990  suplocexprlemell  8044  suplocexprlemmu  8049  suplocexprlemru  8050  suplocexprlemdisj  8051  suplocexprlemloc  8052  suplocexprlemub  8054  suplocexprlemlub  8055  cnm  8163  eluz1  9875  elixx1  10249  elioo2  10273  elfz1  10366  elfzp1  10428  fzpr  10433  fzsuc2  10435  fzrev3  10443  elfzp12  10455  fzm1  10456  fzoval  10504  elfzo  10505  fzodcel  10509  elfzom1b  10596  fzosplitsni  10603  nninfdcex  10621  zmodidfzo  10739  frecuzrdgtcl  10798  frecuzrdgfunlem  10805  seqf1og  10907  bcval  11136  bcpasc  11153  fundm2domnop0  11245  wrdmap  11281  elovmpowrd  11291  ccatfvalfi  11305  elfzelfzccat  11313  ccatlid  11319  ccatass  11321  ccatrn  11322  ccatalpha  11326  swrdfv2  11380  ccatswrd  11387  swrdccat2  11388  pfxfv  11401  pfxeq  11413  ccatpfx  11418  swrdswrd  11422  swrdpfx  11424  pfxpfx  11425  cats1un  11438  swrdccatfn  11441  swrdccatin1  11442  pfxccatin12lem4  11443  pfxccatin12lem1  11445  swrdccatin2  11446  pfxccatin12lem2c  11447  pfxccatin12lem2  11448  swrdccat3blem  11456  swrdccatin1d  11460  swrdccatin2d  11461  pfxccatin12d  11462  shftfn  11534  shftval  11535  seq3shft  11548  iser3shft  12056  sumeq1  12065  summodclem3  12091  summodclem2a  12092  isumss  12102  fsumsplit  12118  sumsplitdc  12143  fsum2dlemstep  12145  fisumcom2  12149  fsumparts  12181  explecnv  12216  fprodsplitdc  12307  fprodsplit  12308  fprod2dlemstep  12333  fprodcom2fi  12337  eftlub  12401  divalgmod  12638  bitsval  12654  bitsp1e  12663  bitsp1o  12664  algfx  12774  eucalgcvga  12780  reumodprminv  12976  nnnn0modprm0  12978  ballotfilemfc0  13176  ballotfilemfcc  13177  ballotfilemsima  13203  ballotfilemrv  13207  ennnfonelemex  13249  ennnfonelemhom  13250  ennnfonelemf1  13253  ennnfonelemrn  13254  ctinfomlemom  13262  ctinfom  13263  ctiunctlemudc  13272  ctiunctlemf  13273  elrest  13543  ptex  13561  imasaddfnlemg  13578  divsfval  13592  xpscf  13611  grpidvalg  13636  grpidpropdg  13637  grpidd  13646  issgrpd  13675  sgrppropd  13676  ismndd  13698  mndpropd  13701  imasmnd2  13707  imasmnd  13708  ismhm  13716  issubm  13727  imasgrp2  13863  imasgrp  13864  issubg  13926  subginv  13934  isnsg  13955  eqg0el  13982  quselbasg  13983  isghm  13996  resghm2b  14015  conjnmzb  14033  conjnsg  14034  ghmpropd  14036  imasabl  14089  gsumsplit0  14099  prdsbasmpt  14122  prdsbasmpt2  14130  pwselbasb  14148  isrngd  14192  rngpropd  14194  imasrng  14195  qusrng  14197  rng1zrlem  14198  dfur2g  14205  srgidmlem  14221  issrgid  14224  ringcl  14256  isringid  14268  isringd  14284  imasring  14307  oppr0g  14325  oppr1g  14326  dvdsrvald  14338  isunitd  14351  unitinvcl  14368  unitinvinv  14369  unitlinv  14371  unitrinv  14372  unitnegcl  14375  dvdsrpropdg  14392  isrhm  14403  isrim0  14406  rhmmul  14409  islring  14437  opprlring  14442  issubrng  14445  opprsubrngg  14457  issubrg  14467  resrhm2b  14495  rhmpropd  14500  rrgval  14508  aprval  14529  aprap  14536  aprprop  14539  islmod  14565  lmodprop2d  14622  islssm  14631  islssmg  14632  islssmd  14633  lssats2  14688  ellspsn  14691  ixpsnbasval  14740  islidlm  14753  isridlrng  14756  rspssp  14768  rnglidlmmgm  14770  2idlval  14776  isridl  14778  2idlelb  14779  quscrng  14807  rspsn  14808  zrhval  14891  zrhrhmb  14896  znf1o  14925  psrgrp  14966  mplelbascoe  14973  istopon  15004  eltg  15043  eltg2  15044  eltop  15060  eltop2  15061  eltop3  15062  iscld  15094  neiss2  15133  isnei  15135  lmfval  15184  cnfval  15185  iscn  15188  iscnp  15190  tgcn  15199  tgcnp  15200  lmbrf  15206  cnptopresti  15229  txbas  15249  eltx  15250  txdis  15268  txdis1cn  15269  hmeofvalg  15294  ishmeo  15295  ispsmet  15314  ismet  15335  isxmet  15336  elblps  15381  elbl  15382  elmopn  15437  neibl  15482  metrest  15497  txmetcnp  15509  txmetcn  15510  metcnpd  15511  elcncf  15564  ellimc3apf  15651  limcmpted  15654  cnlimcim  15662  cnlimc  15663  eldvap  15673  dvidsslem  15684  dviaddf  15696  dvimulf  15697  elply  15725  ply1termlem  15733  lgseisenlem3  16071  edgval  16181  edgiedgbg  16186  edgupgren  16262  upgredg  16265  uhgr2edg  16327  umgr2edg1  16330  usgredg2vlem1  16343  usgredg2vlem2  16344  ushgredgedg  16347  ushgredgedgloop  16349  subgruhgredgdm  16391  uhgrspansubgrlem  16397  vtxdgfval  16409  vtxedgfi  16410  vtxdgop  16413  vtxdg0v  16415  vtxdeqd  16417  vtxdfifiun  16418  1loopgrvd0fi  16427  1hevtxdg0fi  16428  1hevtxdg1en  16429  wksfval  16443  iswlk  16444  wlkm  16460  uspgr2wlkeq  16486  wlkreslem  16499  wlkres  16500  istrl  16506  clwwlkg  16514  isclwwlk  16515  clwwlkccatlem  16521  isclwwlkng  16527  clwwlkn0  16529  clwwlknnn  16533  clwwlkext2edg  16543  clwwlknonmpo  16549  clwwlknon  16550  clwwlk0on0  16552  iseupth  16568  eupth2lem3lem3fi  16591  eupth2lem3lem6fi  16592  eupth2lem3lem4fi  16594  eupth2lembfi  16598  bj-sels  16810  pw1map  16895  nninfall  16913  nninfsellemeq  16918