Theorem eleq2d 2259

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

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

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 2171

This theorem depends on definitions:  df-bi 117  df-cleq 2182  df-clel 2185

This theorem is referenced by:  eleq12d  2260  eleqtrd  2268  neleqtrd  2287  neleqtrrd  2288  abeq2d  2302  nfceqdf  2331  drnfc1  2349  drnfc2  2350  sbcbid  3035  cbvcsbw  3076  cbvcsb  3077  sbcel1g  3091  csbeq2d  3097  csbie2g  3122  cbvralcsf  3134  cbvrexcsf  3135  cbvreucsf  3136  cbvrabcsf  3137  opeq1  3793  opeq2  3794  cbviun  3938  cbviin  3939  iinxsng  3975  iinxprg  3976  iunxsng  3977  iunxsngf  3979  cbvdisj  4005  disjnim  4009  disjiun  4013  mpteq12f  4098  axpweq  4186  rabxfrd  4484  onsucelsucexmid  4544  ordsucunielexmid  4545  0elsucexmid  4579  0nelelxp  4670  opeliunxp  4696  opeliunxp2  4782  iunxpf  4790  elrelimasn  5009  elimasng  5011  xpimasn  5092  ressn  5184  funfni  5331  fnbr  5333  fun11iun  5497  fvelrnb  5579  foelcdmi  5584  fvun1  5598  fvco2  5601  elfvmptrab1  5626  elfvmptrab  5627  elpreima  5651  dff3im  5677  resflem  5696  fmptco  5698  funfvima3  5766  foima2  5768  eluniimadm  5782  dff13  5785  f1eqcocnv  5808  isoini  5835  riotaeqdv  5848  mpoeq123dva  5952  cbvmpox  5969  ovelrn  6040  elovmpod  6089  elovmpo  6090  fmpox  6219  disjxp1  6255  opeliunxp2f  6257  mpoxopn0yelv  6258  mpoxopovel  6260  rbropapd  6261  rntpos  6276  smoel  6319  smoiso  6321  smoel2  6322  tfrlem9  6338  tfrlemisucaccv  6344  tfrlemiubacc  6349  tfrlemi14d  6352  tfri2d  6355  tfr1onlemubacc  6365  tfr1onlemres  6368  tfrcllemubacc  6378  tfrcllemres  6381  rdgon  6405  freceq1  6411  freceq2  6412  frec0g  6416  frecabcl  6418  freccllem  6421  frecfcllem  6423  frecsuclem  6425  frecsuc  6426  nnsucelsuc  6510  nnsucuniel  6514  nnmordi  6535  ereldm  6596  iinerm  6625  elmapg  6679  elpmg  6682  elixpsn  6753  ixpsnf1o  6754  phplem4  6873  phplem3g  6874  phplem4on  6885  exmidpw  6926  fiintim  6946  fidcenumlemrks  6970  fidcenumlemrk  6971  elfi  6988  ordiso2  7052  ctssdccl  7128  nnnninfeq  7144  cc2lem  7283  cc2  7284  cc3  7285  archnqq  7434  ltdfpr  7523  genpelxp  7528  genpelvl  7529  genpelvu  7530  addcanprleml  7631  addcanprlemu  7632  cauappcvgprlem1  7676  suplocexprlemell  7730  suplocexprlemmu  7735  suplocexprlemru  7736  suplocexprlemdisj  7737  suplocexprlemloc  7738  suplocexprlemub  7740  suplocexprlemlub  7741  cnm  7849  eluz1  9550  elixx1  9915  elioo2  9939  elfz1  10031  elfzp1  10090  fzpr  10095  fzsuc2  10097  fzrev3  10105  elfzp12  10117  fzm1  10118  fzoval  10166  elfzo  10167  fzodcel  10170  elfzom1b  10247  fzosplitsni  10253  zmodidfzo  10371  frecuzrdgtcl  10430  frecuzrdgfunlem  10437  bcval  10747  bcpasc  10764  shftfn  10851  shftval  10852  seq3shft  10865  iser3shft  11372  sumeq1  11381  summodclem3  11406  summodclem2a  11407  isumss  11417  fsumsplit  11433  sumsplitdc  11458  fsum2dlemstep  11460  fisumcom2  11464  fsumparts  11496  explecnv  11531  fprodsplitdc  11622  fprodsplit  11623  fprod2dlemstep  11648  fprodcom2fi  11652  eftlub  11716  divalgmod  11950  nninfdcex  11972  algfx  12070  eucalgcvga  12076  reumodprminv  12271  nnnn0modprm0  12273  ennnfonelemex  12433  ennnfonelemhom  12434  ennnfonelemf1  12437  ennnfonelemrn  12438  ctinfomlemom  12446  ctinfom  12447  ctiunctlemudc  12456  ctiunctlemf  12457  elrest  12717  ptex  12735  imasaddfnlemg  12757  xpscf  12789  grpidvalg  12815  grpidpropdg  12816  grpidd  12825  issgrpd  12841  sgrppropd  12842  ismndd  12864  mndpropd  12867  ismhm  12879  issubm  12890  imasgrp2  13018  imasgrp  13019  issubg  13078  subginv  13086  isnsg  13107  eqg0el  13134  quselbasg  13135  isghm  13143  resghm2b  13162  conjnmzb  13180  conjnsg  13181  ghmpropd  13183  imasabl  13234  isrngd  13268  rngpropd  13270  imasrng  13271  qusrng  13273  dfur2g  13277  srgidmlem  13293  issrgid  13296  ringcl  13328  isringid  13340  isringd  13356  imasring  13375  oppr0g  13392  oppr1g  13393  reldvdsrsrg  13403  dvdsrvald  13404  isunitd  13417  unitinvcl  13434  unitinvinv  13435  unitlinv  13437  unitrinv  13438  unitnegcl  13441  dvdsrpropdg  13458  isrhm  13469  isrim0  13472  rhmmul  13475  islring  13500  issubrng  13507  opprsubrngg  13519  issubrg  13529  aprval  13559  aprap  13563  islmod  13568  lmodprop2d  13625  islssm  13634  islssmg  13635  islssmd  13636  lssats2  13691  lspsnel  13694  ixpsnbasval  13743  islidlm  13756  isridlrng  13759  rspssp  13771  rnglidlmmgm  13773  isridl  13780  2idlelb  13781  quscrng  13808  zrhrhmb  13880  istopon  13910  eltg  13949  eltg2  13950  eltop  13966  eltop2  13967  eltop3  13968  iscld  14000  neiss2  14039  isnei  14041  lmfval  14089  cnfval  14091  iscn  14094  iscnp  14096  tgcn  14105  tgcnp  14106  lmbrf  14112  cnptopresti  14135  txbas  14155  eltx  14156  txdis  14174  txdis1cn  14175  hmeofvalg  14200  ishmeo  14201  ispsmet  14220  ismet  14241  isxmet  14242  elblps  14287  elbl  14288  elmopn  14343  neibl  14388  metrest  14403  txmetcnp  14415  txmetcn  14416  metcnpd  14417  elcncf  14457  ellimc3apf  14526  limcmpted  14529  cnlimcim  14537  cnlimc  14538  eldvap  14548  dviaddf  14566  dvimulf  14567  bj-sels  15063  nninfall  15156  nninfsellemeq  15161