Theorem eleq2d 2301

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1397   ∈ wcel 2202

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-clel 2227

This theorem is referenced by:  eleq12d  2302  eleqtrd  2310  neleqtrd  2329  neleqtrrd  2330  abeq2d  2344  nfceqdf  2373  drnfc1  2391  drnfc2  2392  sbcbid  3089  cbvcsbw  3131  cbvcsb  3132  sbcel1g  3146  csbeq2d  3152  csbie2g  3178  cbvralcsf  3190  cbvrexcsf  3191  cbvreucsf  3192  cbvrabcsf  3193  rabsnif  3738  opeq1  3862  opeq2  3863  cbviun  4007  cbviin  4008  iinxsng  4044  iinxprg  4045  iunxsng  4046  iunxsngf  4048  cbvdisj  4074  disjnim  4078  disjiun  4083  mpteq12f  4169  axpweq  4261  rabxfrd  4566  onsucelsucexmid  4628  ordsucunielexmid  4629  0elsucexmid  4663  0nelelxp  4754  opeliunxp  4781  opeliunxp2  4870  iunxpf  4878  elrelimasn  5102  elimasng  5104  xpimasn  5185  ressn  5277  funfni  5432  fnbr  5434  fun11iun  5604  fvelrnb  5693  foelcdmi  5698  fvun1  5712  fvco2  5715  elfvmptrab1  5741  elfvmptrab  5742  elpreima  5766  dff3im  5792  resflem  5811  fmptco  5813  funfvima3  5887  foima2  5891  eluniimadm  5905  dff13  5908  f1eqcocnv  5931  isoini  5958  riotaeqdv  5971  mpoeq123dva  6081  cbvmpox  6098  ovelrn  6170  elovmpod  6219  elovmpo  6220  elovmporab  6221  elovmporab1w  6222  fmpox  6364  disjxp1  6400  opeliunxp2f  6403  mpoxopn0yelv  6404  mpoxopovel  6406  rbropapd  6407  rntpos  6422  smoel  6465  smoiso  6467  smoel2  6468  tfrlem9  6484  tfrlemisucaccv  6490  tfrlemiubacc  6495  tfrlemi14d  6498  tfri2d  6501  tfr1onlemubacc  6511  tfr1onlemres  6514  tfrcllemubacc  6524  tfrcllemres  6527  rdgon  6551  freceq1  6557  freceq2  6558  frec0g  6562  frecabcl  6564  freccllem  6567  frecfcllem  6569  frecsuclem  6571  frecsuc  6572  nnsucelsuc  6658  nnsucuniel  6662  nnmordi  6683  ereldm  6746  iinerm  6775  elmapg  6829  elpmg  6832  elixpsn  6903  ixpsnf1o  6904  pw2f1odclem  7019  phplem4  7040  phplem3g  7041  phplem4on  7053  exmidpw  7099  fiintim  7122  fidcenumlemrks  7151  fidcenumlemrk  7152  elfi  7169  ordiso2  7233  ctssdccl  7309  nnnninfeq  7326  cc2lem  7484  cc2  7485  cc3  7486  archnqq  7636  ltdfpr  7725  genpelxp  7730  genpelvl  7731  genpelvu  7732  addcanprleml  7833  addcanprlemu  7834  cauappcvgprlem1  7878  suplocexprlemell  7932  suplocexprlemmu  7937  suplocexprlemru  7938  suplocexprlemdisj  7939  suplocexprlemloc  7940  suplocexprlemub  7942  suplocexprlemlub  7943  cnm  8051  eluz1  9758  elixx1  10131  elioo2  10155  elfz1  10247  elfzp1  10306  fzpr  10311  fzsuc2  10313  fzrev3  10321  elfzp12  10333  fzm1  10334  fzoval  10382  elfzo  10383  fzodcel  10387  elfzom1b  10473  fzosplitsni  10480  nninfdcex  10496  zmodidfzo  10614  frecuzrdgtcl  10673  frecuzrdgfunlem  10680  seqf1og  10782  bcval  11010  bcpasc  11027  fundm2domnop0  11108  wrdmap  11144  elovmpowrd  11154  ccatfvalfi  11168  elfzelfzccat  11176  ccatlid  11182  ccatass  11184  ccatrn  11185  ccatalpha  11189  swrdfv2  11243  ccatswrd  11250  swrdccat2  11251  pfxfv  11264  pfxeq  11276  ccatpfx  11281  swrdswrd  11285  swrdpfx  11287  pfxpfx  11288  cats1un  11301  swrdccatfn  11304  swrdccatin1  11305  pfxccatin12lem4  11306  pfxccatin12lem1  11308  swrdccatin2  11309  pfxccatin12lem2c  11310  pfxccatin12lem2  11311  swrdccat3blem  11319  swrdccatin1d  11323  swrdccatin2d  11324  pfxccatin12d  11325  shftfn  11384  shftval  11385  seq3shft  11398  iser3shft  11906  sumeq1  11915  summodclem3  11940  summodclem2a  11941  isumss  11951  fsumsplit  11967  sumsplitdc  11992  fsum2dlemstep  11994  fisumcom2  11998  fsumparts  12030  explecnv  12065  fprodsplitdc  12156  fprodsplit  12157  fprod2dlemstep  12182  fprodcom2fi  12186  eftlub  12250  divalgmod  12487  bitsval  12503  bitsp1e  12512  bitsp1o  12513  algfx  12623  eucalgcvga  12629  reumodprminv  12825  nnnn0modprm0  12827  ennnfonelemex  13034  ennnfonelemhom  13035  ennnfonelemf1  13038  ennnfonelemrn  13039  ctinfomlemom  13047  ctinfom  13048  ctiunctlemudc  13057  ctiunctlemf  13058  elrest  13328  ptex  13346  prdsbasmpt  13362  prdsbasmpt2  13370  pwselbasb  13375  imasaddfnlemg  13396  divsfval  13410  xpscf  13429  grpidvalg  13455  grpidpropdg  13456  grpidd  13465  issgrpd  13494  sgrppropd  13495  ismndd  13519  mndpropd  13522  imasmnd2  13534  imasmnd  13535  ismhm  13543  issubm  13554  imasgrp2  13696  imasgrp  13697  issubg  13759  subginv  13767  isnsg  13788  eqg0el  13815  quselbasg  13816  isghm  13829  resghm2b  13848  conjnmzb  13866  conjnsg  13867  ghmpropd  13869  imasabl  13922  isrngd  13965  rngpropd  13967  imasrng  13968  qusrng  13970  dfur2g  13974  srgidmlem  13990  issrgid  13993  ringcl  14025  isringid  14037  isringd  14053  imasring  14076  oppr0g  14093  oppr1g  14094  dvdsrvald  14106  isunitd  14119  unitinvcl  14136  unitinvinv  14137  unitlinv  14139  unitrinv  14140  unitnegcl  14143  dvdsrpropdg  14160  isrhm  14171  isrim0  14174  rhmmul  14177  islring  14205  issubrng  14212  opprsubrngg  14224  issubrg  14234  resrhm2b  14262  rhmpropd  14267  rrgval  14275  aprval  14295  aprap  14299  islmod  14304  lmodprop2d  14361  islssm  14370  islssmg  14371  islssmd  14372  lssats2  14427  ellspsn  14430  ixpsnbasval  14479  islidlm  14492  isridlrng  14495  rspssp  14507  rnglidlmmgm  14509  2idlval  14515  isridl  14517  2idlelb  14518  quscrng  14546  rspsn  14547  zrhval  14630  zrhrhmb  14635  znf1o  14664  psrgrp  14698  mplelbascoe  14705  istopon  14736  eltg  14775  eltg2  14776  eltop  14792  eltop2  14793  eltop3  14794  iscld  14826  neiss2  14865  isnei  14867  lmfval  14916  cnfval  14917  iscn  14920  iscnp  14922  tgcn  14931  tgcnp  14932  lmbrf  14938  cnptopresti  14961  txbas  14981  eltx  14982  txdis  15000  txdis1cn  15001  hmeofvalg  15026  ishmeo  15027  ispsmet  15046  ismet  15067  isxmet  15068  elblps  15113  elbl  15114  elmopn  15169  neibl  15214  metrest  15229  txmetcnp  15241  txmetcn  15242  metcnpd  15243  elcncf  15296  ellimc3apf  15383  limcmpted  15386  cnlimcim  15394  cnlimc  15395  eldvap  15405  dvidsslem  15416  dviaddf  15428  dvimulf  15429  elply  15457  ply1termlem  15465  lgseisenlem3  15800  edgval  15910  edgiedgbg  15915  edgupgren  15991  upgredg  15994  uhgr2edg  16056  umgr2edg1  16059  usgredg2vlem1  16072  usgredg2vlem2  16073  ushgredgedg  16076  ushgredgedgloop  16078  subgruhgredgdm  16120  uhgrspansubgrlem  16126  vtxdgfval  16138  vtxedgfi  16139  vtxdgop  16142  vtxdg0v  16144  vtxdeqd  16146  vtxdfifiun  16147  1loopgrvd0fi  16156  1hevtxdg0fi  16157  1hevtxdg1en  16158  wksfval  16172  iswlk  16173  wlkm  16189  uspgr2wlkeq  16215  wlkreslem  16228  wlkres  16229  istrl  16235  clwwlkg  16243  isclwwlk  16244  clwwlkccatlem  16250  isclwwlkng  16256  clwwlkn0  16258  clwwlknnn  16262  clwwlkext2edg  16272  clwwlknonmpo  16278  clwwlknon  16279  clwwlk0on0  16281  iseupth  16297  bj-sels  16509  2omap  16594  pw1map  16596  nninfall  16611  nninfsellemeq  16616