Theorem eleq2d 2263

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1364   ∈ wcel 2164

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-cleq 2186  df-clel 2189

This theorem is referenced by:  eleq12d  2264  eleqtrd  2272  neleqtrd  2291  neleqtrrd  2292  abeq2d  2306  nfceqdf  2335  drnfc1  2353  drnfc2  2354  sbcbid  3043  cbvcsbw  3084  cbvcsb  3085  sbcel1g  3099  csbeq2d  3105  csbie2g  3131  cbvralcsf  3143  cbvrexcsf  3144  cbvreucsf  3145  cbvrabcsf  3146  opeq1  3804  opeq2  3805  cbviun  3949  cbviin  3950  iinxsng  3986  iinxprg  3987  iunxsng  3988  iunxsngf  3990  cbvdisj  4016  disjnim  4020  disjiun  4024  mpteq12f  4109  axpweq  4200  rabxfrd  4500  onsucelsucexmid  4562  ordsucunielexmid  4563  0elsucexmid  4597  0nelelxp  4688  opeliunxp  4714  opeliunxp2  4802  iunxpf  4810  elrelimasn  5031  elimasng  5033  xpimasn  5114  ressn  5206  funfni  5354  fnbr  5356  fun11iun  5521  fvelrnb  5604  foelcdmi  5609  fvun1  5623  fvco2  5626  elfvmptrab1  5652  elfvmptrab  5653  elpreima  5677  dff3im  5703  resflem  5722  fmptco  5724  funfvima3  5792  foima2  5794  eluniimadm  5808  dff13  5811  f1eqcocnv  5834  isoini  5861  riotaeqdv  5874  mpoeq123dva  5979  cbvmpox  5996  ovelrn  6067  elovmpod  6116  elovmpo  6117  elovmporab  6118  elovmporab1w  6119  fmpox  6253  disjxp1  6289  opeliunxp2f  6291  mpoxopn0yelv  6292  mpoxopovel  6294  rbropapd  6295  rntpos  6310  smoel  6353  smoiso  6355  smoel2  6356  tfrlem9  6372  tfrlemisucaccv  6378  tfrlemiubacc  6383  tfrlemi14d  6386  tfri2d  6389  tfr1onlemubacc  6399  tfr1onlemres  6402  tfrcllemubacc  6412  tfrcllemres  6415  rdgon  6439  freceq1  6445  freceq2  6446  frec0g  6450  frecabcl  6452  freccllem  6455  frecfcllem  6457  frecsuclem  6459  frecsuc  6460  nnsucelsuc  6544  nnsucuniel  6548  nnmordi  6569  ereldm  6632  iinerm  6661  elmapg  6715  elpmg  6718  elixpsn  6789  ixpsnf1o  6790  pw2f1odclem  6890  phplem4  6911  phplem3g  6912  phplem4on  6923  exmidpw  6964  fiintim  6985  fidcenumlemrks  7012  fidcenumlemrk  7013  elfi  7030  ordiso2  7094  ctssdccl  7170  nnnninfeq  7187  cc2lem  7326  cc2  7327  cc3  7328  archnqq  7477  ltdfpr  7566  genpelxp  7571  genpelvl  7572  genpelvu  7573  addcanprleml  7674  addcanprlemu  7675  cauappcvgprlem1  7719  suplocexprlemell  7773  suplocexprlemmu  7778  suplocexprlemru  7779  suplocexprlemdisj  7780  suplocexprlemloc  7781  suplocexprlemub  7783  suplocexprlemlub  7784  cnm  7892  eluz1  9596  elixx1  9963  elioo2  9987  elfz1  10079  elfzp1  10138  fzpr  10143  fzsuc2  10145  fzrev3  10153  elfzp12  10165  fzm1  10166  fzoval  10214  elfzo  10215  fzodcel  10219  elfzom1b  10296  fzosplitsni  10302  zmodidfzo  10424  frecuzrdgtcl  10483  frecuzrdgfunlem  10490  seqf1og  10592  bcval  10820  bcpasc  10837  wrdmap  10945  elovmpowrd  10955  shftfn  10968  shftval  10969  seq3shft  10982  iser3shft  11489  sumeq1  11498  summodclem3  11523  summodclem2a  11524  isumss  11534  fsumsplit  11550  sumsplitdc  11575  fsum2dlemstep  11577  fisumcom2  11581  fsumparts  11613  explecnv  11648  fprodsplitdc  11739  fprodsplit  11740  fprod2dlemstep  11765  fprodcom2fi  11769  eftlub  11833  divalgmod  12068  nninfdcex  12090  algfx  12190  eucalgcvga  12196  reumodprminv  12391  nnnn0modprm0  12393  ennnfonelemex  12571  ennnfonelemhom  12572  ennnfonelemf1  12575  ennnfonelemrn  12576  ctinfomlemom  12584  ctinfom  12585  ctiunctlemudc  12594  ctiunctlemf  12595  elrest  12857  ptex  12875  imasaddfnlemg  12897  divsfval  12911  xpscf  12930  grpidvalg  12956  grpidpropdg  12957  grpidd  12966  issgrpd  12995  sgrppropd  12996  ismndd  13018  mndpropd  13021  ismhm  13033  issubm  13044  imasgrp2  13180  imasgrp  13181  issubg  13243  subginv  13251  isnsg  13272  eqg0el  13299  quselbasg  13300  isghm  13313  resghm2b  13332  conjnmzb  13350  conjnsg  13351  ghmpropd  13353  imasabl  13406  isrngd  13449  rngpropd  13451  imasrng  13452  qusrng  13454  dfur2g  13458  srgidmlem  13474  issrgid  13477  ringcl  13509  isringid  13521  isringd  13537  imasring  13560  oppr0g  13577  oppr1g  13578  reldvdsrsrg  13588  dvdsrvald  13589  isunitd  13602  unitinvcl  13619  unitinvinv  13620  unitlinv  13622  unitrinv  13623  unitnegcl  13626  dvdsrpropdg  13643  isrhm  13654  isrim0  13657  rhmmul  13660  islring  13688  issubrng  13695  opprsubrngg  13707  issubrg  13717  resrhm2b  13745  rhmpropd  13750  rrgval  13758  aprval  13778  aprap  13782  islmod  13787  lmodprop2d  13844  islssm  13853  islssmg  13854  islssmd  13855  lssats2  13910  ellspsn  13913  ixpsnbasval  13962  islidlm  13975  isridlrng  13978  rspssp  13990  rnglidlmmgm  13992  2idlval  13998  isridl  14000  2idlelb  14001  quscrng  14029  rspsn  14030  zrhval  14105  zrhrhmb  14110  znf1o  14139  istopon  14181  eltg  14220  eltg2  14221  eltop  14237  eltop2  14238  eltop3  14239  iscld  14271  neiss2  14310  isnei  14312  lmfval  14360  cnfval  14362  iscn  14365  iscnp  14367  tgcn  14376  tgcnp  14377  lmbrf  14383  cnptopresti  14406  txbas  14426  eltx  14427  txdis  14445  txdis1cn  14446  hmeofvalg  14471  ishmeo  14472  ispsmet  14491  ismet  14512  isxmet  14513  elblps  14558  elbl  14559  elmopn  14614  neibl  14659  metrest  14674  txmetcnp  14686  txmetcn  14687  metcnpd  14688  elcncf  14728  ellimc3apf  14814  limcmpted  14817  cnlimcim  14825  cnlimc  14826  eldvap  14836  dviaddf  14854  dvimulf  14855  elply  14880  ply1termlem  14888  lgseisenlem3  15188  bj-sels  15406  nninfall  15499  nninfsellemeq  15504