Theorem eleq2d 2299

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1395   ∈ wcel 2200

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-clel 2225

This theorem is referenced by:  eleq12d  2300  eleqtrd  2308  neleqtrd  2327  neleqtrrd  2328  abeq2d  2342  nfceqdf  2371  drnfc1  2389  drnfc2  2390  sbcbid  3086  cbvcsbw  3128  cbvcsb  3129  sbcel1g  3143  csbeq2d  3149  csbie2g  3175  cbvralcsf  3187  cbvrexcsf  3188  cbvreucsf  3189  cbvrabcsf  3190  opeq1  3856  opeq2  3857  cbviun  4001  cbviin  4002  iinxsng  4038  iinxprg  4039  iunxsng  4040  iunxsngf  4042  cbvdisj  4068  disjnim  4072  disjiun  4077  mpteq12f  4163  axpweq  4254  rabxfrd  4559  onsucelsucexmid  4621  ordsucunielexmid  4622  0elsucexmid  4656  0nelelxp  4747  opeliunxp  4773  opeliunxp2  4861  iunxpf  4869  elrelimasn  5093  elimasng  5095  xpimasn  5176  ressn  5268  funfni  5422  fnbr  5424  fun11iun  5592  fvelrnb  5680  foelcdmi  5685  fvun1  5699  fvco2  5702  elfvmptrab1  5728  elfvmptrab  5729  elpreima  5753  dff3im  5779  resflem  5798  fmptco  5800  funfvima3  5872  foima2  5874  eluniimadm  5888  dff13  5891  f1eqcocnv  5914  isoini  5941  riotaeqdv  5954  mpoeq123dva  6064  cbvmpox  6081  ovelrn  6153  elovmpod  6202  elovmpo  6203  elovmporab  6204  elovmporab1w  6205  fmpox  6344  disjxp1  6380  opeliunxp2f  6382  mpoxopn0yelv  6383  mpoxopovel  6385  rbropapd  6386  rntpos  6401  smoel  6444  smoiso  6446  smoel2  6447  tfrlem9  6463  tfrlemisucaccv  6469  tfrlemiubacc  6474  tfrlemi14d  6477  tfri2d  6480  tfr1onlemubacc  6490  tfr1onlemres  6493  tfrcllemubacc  6503  tfrcllemres  6506  rdgon  6530  freceq1  6536  freceq2  6537  frec0g  6541  frecabcl  6543  freccllem  6546  frecfcllem  6548  frecsuclem  6550  frecsuc  6551  nnsucelsuc  6635  nnsucuniel  6639  nnmordi  6660  ereldm  6723  iinerm  6752  elmapg  6806  elpmg  6809  elixpsn  6880  ixpsnf1o  6881  pw2f1odclem  6991  phplem4  7012  phplem3g  7013  phplem4on  7025  exmidpw  7066  fiintim  7089  fidcenumlemrks  7116  fidcenumlemrk  7117  elfi  7134  ordiso2  7198  ctssdccl  7274  nnnninfeq  7291  cc2lem  7448  cc2  7449  cc3  7450  archnqq  7600  ltdfpr  7689  genpelxp  7694  genpelvl  7695  genpelvu  7696  addcanprleml  7797  addcanprlemu  7798  cauappcvgprlem1  7842  suplocexprlemell  7896  suplocexprlemmu  7901  suplocexprlemru  7902  suplocexprlemdisj  7903  suplocexprlemloc  7904  suplocexprlemub  7906  suplocexprlemlub  7907  cnm  8015  eluz1  9722  elixx1  10089  elioo2  10113  elfz1  10205  elfzp1  10264  fzpr  10269  fzsuc2  10271  fzrev3  10279  elfzp12  10291  fzm1  10292  fzoval  10340  elfzo  10341  fzodcel  10345  elfzom1b  10430  fzosplitsni  10436  nninfdcex  10452  zmodidfzo  10570  frecuzrdgtcl  10629  frecuzrdgfunlem  10636  seqf1og  10738  bcval  10966  bcpasc  10983  fundm2domnop0  11062  wrdmap  11098  elovmpowrd  11108  ccatfvalfi  11122  elfzelfzccat  11130  ccatlid  11136  ccatass  11138  ccatrn  11139  swrdfv2  11190  ccatswrd  11197  swrdccat2  11198  pfxfv  11211  pfxeq  11223  ccatpfx  11228  swrdswrd  11232  swrdpfx  11234  pfxpfx  11235  cats1un  11248  swrdccatfn  11251  swrdccatin1  11252  pfxccatin12lem4  11253  pfxccatin12lem1  11255  swrdccatin2  11256  pfxccatin12lem2c  11257  pfxccatin12lem2  11258  swrdccat3blem  11266  swrdccatin1d  11270  swrdccatin2d  11271  pfxccatin12d  11272  shftfn  11330  shftval  11331  seq3shft  11344  iser3shft  11852  sumeq1  11861  summodclem3  11886  summodclem2a  11887  isumss  11897  fsumsplit  11913  sumsplitdc  11938  fsum2dlemstep  11940  fisumcom2  11944  fsumparts  11976  explecnv  12011  fprodsplitdc  12102  fprodsplit  12103  fprod2dlemstep  12128  fprodcom2fi  12132  eftlub  12196  divalgmod  12433  bitsval  12449  bitsp1e  12458  bitsp1o  12459  algfx  12569  eucalgcvga  12575  reumodprminv  12771  nnnn0modprm0  12773  ennnfonelemex  12980  ennnfonelemhom  12981  ennnfonelemf1  12984  ennnfonelemrn  12985  ctinfomlemom  12993  ctinfom  12994  ctiunctlemudc  13003  ctiunctlemf  13004  elrest  13274  ptex  13292  prdsbasmpt  13308  prdsbasmpt2  13316  pwselbasb  13321  imasaddfnlemg  13342  divsfval  13356  xpscf  13375  grpidvalg  13401  grpidpropdg  13402  grpidd  13411  issgrpd  13440  sgrppropd  13441  ismndd  13465  mndpropd  13468  imasmnd2  13480  imasmnd  13481  ismhm  13489  issubm  13500  imasgrp2  13642  imasgrp  13643  issubg  13705  subginv  13713  isnsg  13734  eqg0el  13761  quselbasg  13762  isghm  13775  resghm2b  13794  conjnmzb  13812  conjnsg  13813  ghmpropd  13815  imasabl  13868  isrngd  13911  rngpropd  13913  imasrng  13914  qusrng  13916  dfur2g  13920  srgidmlem  13936  issrgid  13939  ringcl  13971  isringid  13983  isringd  13999  imasring  14022  oppr0g  14039  oppr1g  14040  reldvdsrsrg  14050  dvdsrvald  14051  isunitd  14064  unitinvcl  14081  unitinvinv  14082  unitlinv  14084  unitrinv  14085  unitnegcl  14088  dvdsrpropdg  14105  isrhm  14116  isrim0  14119  rhmmul  14122  islring  14150  issubrng  14157  opprsubrngg  14169  issubrg  14179  resrhm2b  14207  rhmpropd  14212  rrgval  14220  aprval  14240  aprap  14244  islmod  14249  lmodprop2d  14306  islssm  14315  islssmg  14316  islssmd  14317  lssats2  14372  ellspsn  14375  ixpsnbasval  14424  islidlm  14437  isridlrng  14440  rspssp  14452  rnglidlmmgm  14454  2idlval  14460  isridl  14462  2idlelb  14463  quscrng  14491  rspsn  14492  zrhval  14575  zrhrhmb  14580  znf1o  14609  psrgrp  14643  mplelbascoe  14650  istopon  14681  eltg  14720  eltg2  14721  eltop  14737  eltop2  14738  eltop3  14739  iscld  14771  neiss2  14810  isnei  14812  lmfval  14860  cnfval  14862  iscn  14865  iscnp  14867  tgcn  14876  tgcnp  14877  lmbrf  14883  cnptopresti  14906  txbas  14926  eltx  14927  txdis  14945  txdis1cn  14946  hmeofvalg  14971  ishmeo  14972  ispsmet  14991  ismet  15012  isxmet  15013  elblps  15058  elbl  15059  elmopn  15114  neibl  15159  metrest  15174  txmetcnp  15186  txmetcn  15187  metcnpd  15188  elcncf  15241  ellimc3apf  15328  limcmpted  15331  cnlimcim  15339  cnlimc  15340  eldvap  15350  dvidsslem  15361  dviaddf  15373  dvimulf  15374  elply  15402  ply1termlem  15410  lgseisenlem3  15745  edgiedgbg  15859  edgupgren  15933  upgredg  15936  uhgr2edg  15998  umgr2edg1  16001  usgredg2vlem1  16014  usgredg2vlem2  16015  ushgredgedg  16018  ushgredgedgloop  16020  wksfval  16028  iswlk  16029  wlkm  16038  bj-sels  16235  2omap  16318  pw1map  16320  nninfall  16334  nninfsellemeq  16339