Theorem eleq2d 2274

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1372   ∈ wcel 2175

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 1469  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-4 1532  ax-17 1548  ax-ial 1556  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-cleq 2197  df-clel 2200

This theorem is referenced by:  eleq12d  2275  eleqtrd  2283  neleqtrd  2302  neleqtrrd  2303  abeq2d  2317  nfceqdf  2346  drnfc1  2364  drnfc2  2365  sbcbid  3055  cbvcsbw  3096  cbvcsb  3097  sbcel1g  3111  csbeq2d  3117  csbie2g  3143  cbvralcsf  3155  cbvrexcsf  3156  cbvreucsf  3157  cbvrabcsf  3158  opeq1  3818  opeq2  3819  cbviun  3963  cbviin  3964  iinxsng  4000  iinxprg  4001  iunxsng  4002  iunxsngf  4004  cbvdisj  4030  disjnim  4034  disjiun  4038  mpteq12f  4123  axpweq  4214  rabxfrd  4514  onsucelsucexmid  4576  ordsucunielexmid  4577  0elsucexmid  4611  0nelelxp  4702  opeliunxp  4728  opeliunxp2  4816  iunxpf  4824  elrelimasn  5045  elimasng  5047  xpimasn  5128  ressn  5220  funfni  5370  fnbr  5372  fun11iun  5537  fvelrnb  5620  foelcdmi  5625  fvun1  5639  fvco2  5642  elfvmptrab1  5668  elfvmptrab  5669  elpreima  5693  dff3im  5719  resflem  5738  fmptco  5740  funfvima3  5808  foima2  5810  eluniimadm  5824  dff13  5827  f1eqcocnv  5850  isoini  5877  riotaeqdv  5890  mpoeq123dva  5996  cbvmpox  6013  ovelrn  6085  elovmpod  6134  elovmpo  6135  elovmporab  6136  elovmporab1w  6137  fmpox  6276  disjxp1  6312  opeliunxp2f  6314  mpoxopn0yelv  6315  mpoxopovel  6317  rbropapd  6318  rntpos  6333  smoel  6376  smoiso  6378  smoel2  6379  tfrlem9  6395  tfrlemisucaccv  6401  tfrlemiubacc  6406  tfrlemi14d  6409  tfri2d  6412  tfr1onlemubacc  6422  tfr1onlemres  6425  tfrcllemubacc  6435  tfrcllemres  6438  rdgon  6462  freceq1  6468  freceq2  6469  frec0g  6473  frecabcl  6475  freccllem  6478  frecfcllem  6480  frecsuclem  6482  frecsuc  6483  nnsucelsuc  6567  nnsucuniel  6571  nnmordi  6592  ereldm  6655  iinerm  6684  elmapg  6738  elpmg  6741  elixpsn  6812  ixpsnf1o  6813  pw2f1odclem  6913  phplem4  6934  phplem3g  6935  phplem4on  6946  exmidpw  6987  fiintim  7010  fidcenumlemrks  7037  fidcenumlemrk  7038  elfi  7055  ordiso2  7119  ctssdccl  7195  nnnninfeq  7212  cc2lem  7360  cc2  7361  cc3  7362  archnqq  7512  ltdfpr  7601  genpelxp  7606  genpelvl  7607  genpelvu  7608  addcanprleml  7709  addcanprlemu  7710  cauappcvgprlem1  7754  suplocexprlemell  7808  suplocexprlemmu  7813  suplocexprlemru  7814  suplocexprlemdisj  7815  suplocexprlemloc  7816  suplocexprlemub  7818  suplocexprlemlub  7819  cnm  7927  eluz1  9634  elixx1  10001  elioo2  10025  elfz1  10117  elfzp1  10176  fzpr  10181  fzsuc2  10183  fzrev3  10191  elfzp12  10203  fzm1  10204  fzoval  10252  elfzo  10253  fzodcel  10257  elfzom1b  10339  fzosplitsni  10345  nninfdcex  10361  zmodidfzo  10479  frecuzrdgtcl  10538  frecuzrdgfunlem  10545  seqf1og  10647  bcval  10875  bcpasc  10892  wrdmap  11000  elovmpowrd  11010  ccatfvalfi  11023  elfzelfzccat  11031  ccatlid  11037  ccatass  11039  ccatrn  11040  shftfn  11054  shftval  11055  seq3shft  11068  iser3shft  11576  sumeq1  11585  summodclem3  11610  summodclem2a  11611  isumss  11621  fsumsplit  11637  sumsplitdc  11662  fsum2dlemstep  11664  fisumcom2  11668  fsumparts  11700  explecnv  11735  fprodsplitdc  11826  fprodsplit  11827  fprod2dlemstep  11852  fprodcom2fi  11856  eftlub  11920  divalgmod  12157  bitsval  12173  bitsp1e  12182  bitsp1o  12183  algfx  12293  eucalgcvga  12299  reumodprminv  12495  nnnn0modprm0  12497  ennnfonelemex  12704  ennnfonelemhom  12705  ennnfonelemf1  12708  ennnfonelemrn  12709  ctinfomlemom  12717  ctinfom  12718  ctiunctlemudc  12727  ctiunctlemf  12728  elrest  12996  ptex  13014  prdsbasmpt  13030  prdsbasmpt2  13038  pwselbasb  13043  imasaddfnlemg  13064  divsfval  13078  xpscf  13097  grpidvalg  13123  grpidpropdg  13124  grpidd  13133  issgrpd  13162  sgrppropd  13163  ismndd  13187  mndpropd  13190  imasmnd2  13202  imasmnd  13203  ismhm  13211  issubm  13222  imasgrp2  13364  imasgrp  13365  issubg  13427  subginv  13435  isnsg  13456  eqg0el  13483  quselbasg  13484  isghm  13497  resghm2b  13516  conjnmzb  13534  conjnsg  13535  ghmpropd  13537  imasabl  13590  isrngd  13633  rngpropd  13635  imasrng  13636  qusrng  13638  dfur2g  13642  srgidmlem  13658  issrgid  13661  ringcl  13693  isringid  13705  isringd  13721  imasring  13744  oppr0g  13761  oppr1g  13762  reldvdsrsrg  13772  dvdsrvald  13773  isunitd  13786  unitinvcl  13803  unitinvinv  13804  unitlinv  13806  unitrinv  13807  unitnegcl  13810  dvdsrpropdg  13827  isrhm  13838  isrim0  13841  rhmmul  13844  islring  13872  issubrng  13879  opprsubrngg  13891  issubrg  13901  resrhm2b  13929  rhmpropd  13934  rrgval  13942  aprval  13962  aprap  13966  islmod  13971  lmodprop2d  14028  islssm  14037  islssmg  14038  islssmd  14039  lssats2  14094  ellspsn  14097  ixpsnbasval  14146  islidlm  14159  isridlrng  14162  rspssp  14174  rnglidlmmgm  14176  2idlval  14182  isridl  14184  2idlelb  14185  quscrng  14213  rspsn  14214  zrhval  14297  zrhrhmb  14302  znf1o  14331  psrgrp  14365  mplelbascoe  14372  istopon  14403  eltg  14442  eltg2  14443  eltop  14459  eltop2  14460  eltop3  14461  iscld  14493  neiss2  14532  isnei  14534  lmfval  14582  cnfval  14584  iscn  14587  iscnp  14589  tgcn  14598  tgcnp  14599  lmbrf  14605  cnptopresti  14628  txbas  14648  eltx  14649  txdis  14667  txdis1cn  14668  hmeofvalg  14693  ishmeo  14694  ispsmet  14713  ismet  14734  isxmet  14735  elblps  14780  elbl  14781  elmopn  14836  neibl  14881  metrest  14896  txmetcnp  14908  txmetcn  14909  metcnpd  14910  elcncf  14963  ellimc3apf  15050  limcmpted  15053  cnlimcim  15061  cnlimc  15062  eldvap  15072  dvidsslem  15083  dviaddf  15095  dvimulf  15096  elply  15124  ply1termlem  15132  lgseisenlem3  15467  bj-sels  15714  2omap  15796  nninfall  15810  nninfsellemeq  15815