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  4515  onsucelsucexmid  4577  ordsucunielexmid  4578  0elsucexmid  4612  0nelelxp  4703  opeliunxp  4729  opeliunxp2  4817  iunxpf  4825  elrelimasn  5047  elimasng  5049  xpimasn  5130  ressn  5222  funfni  5375  fnbr  5377  fun11iun  5542  fvelrnb  5625  foelcdmi  5630  fvun1  5644  fvco2  5647  elfvmptrab1  5673  elfvmptrab  5674  elpreima  5698  dff3im  5724  resflem  5743  fmptco  5745  funfvima3  5817  foima2  5819  eluniimadm  5833  dff13  5836  f1eqcocnv  5859  isoini  5886  riotaeqdv  5899  mpoeq123dva  6005  cbvmpox  6022  ovelrn  6094  elovmpod  6143  elovmpo  6144  elovmporab  6145  elovmporab1w  6146  fmpox  6285  disjxp1  6321  opeliunxp2f  6323  mpoxopn0yelv  6324  mpoxopovel  6326  rbropapd  6327  rntpos  6342  smoel  6385  smoiso  6387  smoel2  6388  tfrlem9  6404  tfrlemisucaccv  6410  tfrlemiubacc  6415  tfrlemi14d  6418  tfri2d  6421  tfr1onlemubacc  6431  tfr1onlemres  6434  tfrcllemubacc  6444  tfrcllemres  6447  rdgon  6471  freceq1  6477  freceq2  6478  frec0g  6482  frecabcl  6484  freccllem  6487  frecfcllem  6489  frecsuclem  6491  frecsuc  6492  nnsucelsuc  6576  nnsucuniel  6580  nnmordi  6601  ereldm  6664  iinerm  6693  elmapg  6747  elpmg  6750  elixpsn  6821  ixpsnf1o  6822  pw2f1odclem  6930  phplem4  6951  phplem3g  6952  phplem4on  6963  exmidpw  7004  fiintim  7027  fidcenumlemrks  7054  fidcenumlemrk  7055  elfi  7072  ordiso2  7136  ctssdccl  7212  nnnninfeq  7229  cc2lem  7377  cc2  7378  cc3  7379  archnqq  7529  ltdfpr  7618  genpelxp  7623  genpelvl  7624  genpelvu  7625  addcanprleml  7726  addcanprlemu  7727  cauappcvgprlem1  7771  suplocexprlemell  7825  suplocexprlemmu  7830  suplocexprlemru  7831  suplocexprlemdisj  7832  suplocexprlemloc  7833  suplocexprlemub  7835  suplocexprlemlub  7836  cnm  7944  eluz1  9651  elixx1  10018  elioo2  10042  elfz1  10134  elfzp1  10193  fzpr  10198  fzsuc2  10200  fzrev3  10208  elfzp12  10220  fzm1  10221  fzoval  10269  elfzo  10270  fzodcel  10274  elfzom1b  10356  fzosplitsni  10362  nninfdcex  10378  zmodidfzo  10496  frecuzrdgtcl  10555  frecuzrdgfunlem  10562  seqf1og  10664  bcval  10892  bcpasc  10909  fundm2domnop0  10988  wrdmap  11023  elovmpowrd  11033  ccatfvalfi  11046  elfzelfzccat  11054  ccatlid  11060  ccatass  11062  ccatrn  11063  shftfn  11077  shftval  11078  seq3shft  11091  iser3shft  11599  sumeq1  11608  summodclem3  11633  summodclem2a  11634  isumss  11644  fsumsplit  11660  sumsplitdc  11685  fsum2dlemstep  11687  fisumcom2  11691  fsumparts  11723  explecnv  11758  fprodsplitdc  11849  fprodsplit  11850  fprod2dlemstep  11875  fprodcom2fi  11879  eftlub  11943  divalgmod  12180  bitsval  12196  bitsp1e  12205  bitsp1o  12206  algfx  12316  eucalgcvga  12322  reumodprminv  12518  nnnn0modprm0  12520  ennnfonelemex  12727  ennnfonelemhom  12728  ennnfonelemf1  12731  ennnfonelemrn  12732  ctinfomlemom  12740  ctinfom  12741  ctiunctlemudc  12750  ctiunctlemf  12751  elrest  13020  ptex  13038  prdsbasmpt  13054  prdsbasmpt2  13062  pwselbasb  13067  imasaddfnlemg  13088  divsfval  13102  xpscf  13121  grpidvalg  13147  grpidpropdg  13148  grpidd  13157  issgrpd  13186  sgrppropd  13187  ismndd  13211  mndpropd  13214  imasmnd2  13226  imasmnd  13227  ismhm  13235  issubm  13246  imasgrp2  13388  imasgrp  13389  issubg  13451  subginv  13459  isnsg  13480  eqg0el  13507  quselbasg  13508  isghm  13521  resghm2b  13540  conjnmzb  13558  conjnsg  13559  ghmpropd  13561  imasabl  13614  isrngd  13657  rngpropd  13659  imasrng  13660  qusrng  13662  dfur2g  13666  srgidmlem  13682  issrgid  13685  ringcl  13717  isringid  13729  isringd  13745  imasring  13768  oppr0g  13785  oppr1g  13786  reldvdsrsrg  13796  dvdsrvald  13797  isunitd  13810  unitinvcl  13827  unitinvinv  13828  unitlinv  13830  unitrinv  13831  unitnegcl  13834  dvdsrpropdg  13851  isrhm  13862  isrim0  13865  rhmmul  13868  islring  13896  issubrng  13903  opprsubrngg  13915  issubrg  13925  resrhm2b  13953  rhmpropd  13958  rrgval  13966  aprval  13986  aprap  13990  islmod  13995  lmodprop2d  14052  islssm  14061  islssmg  14062  islssmd  14063  lssats2  14118  ellspsn  14121  ixpsnbasval  14170  islidlm  14183  isridlrng  14186  rspssp  14198  rnglidlmmgm  14200  2idlval  14206  isridl  14208  2idlelb  14209  quscrng  14237  rspsn  14238  zrhval  14321  zrhrhmb  14326  znf1o  14355  psrgrp  14389  mplelbascoe  14396  istopon  14427  eltg  14466  eltg2  14467  eltop  14483  eltop2  14484  eltop3  14485  iscld  14517  neiss2  14556  isnei  14558  lmfval  14606  cnfval  14608  iscn  14611  iscnp  14613  tgcn  14622  tgcnp  14623  lmbrf  14629  cnptopresti  14652  txbas  14672  eltx  14673  txdis  14691  txdis1cn  14692  hmeofvalg  14717  ishmeo  14718  ispsmet  14737  ismet  14758  isxmet  14759  elblps  14804  elbl  14805  elmopn  14860  neibl  14905  metrest  14920  txmetcnp  14932  txmetcn  14933  metcnpd  14934  elcncf  14987  ellimc3apf  15074  limcmpted  15077  cnlimcim  15085  cnlimc  15086  eldvap  15096  dvidsslem  15107  dviaddf  15119  dvimulf  15120  elply  15148  ply1termlem  15156  lgseisenlem3  15491  bj-sels  15783  2omap  15865  nninfall  15879  nninfsellemeq  15884