NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  eleq1d GIF version

Theorem eleq1d 2419
Description: Deduction from equality to equivalence of membership. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
eleq1d.1 (φA = B)
Assertion
Ref Expression
eleq1d (φ → (A CB C))

Proof of Theorem eleq1d
StepHypRef Expression
1 eleq1d.1 . 2 (φA = B)
2 eleq1 2413 . 2 (A = B → (A CB C))
31, 2syl 15 1 (φ → (A CB C))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 176   = wceq 1642   wcel 1710
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746  ax-ext 2334
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-cleq 2346  df-clel 2349
This theorem is referenced by:  eleq12d  2421  eqeltrd  2427  eqneltrd  2446  eqneltrrd  2447  rspcimdv  2956  reuind  3039  sbcel2g  3157  sbccsb2g  3165  ifexg  3721  ninexg  4097  snex  4111  snel1cg  4141  eluni1g  4172  opkelcnvkg  4249  otkelins2kg  4253  otkelins3kg  4254  elimakg  4257  opkelcokg  4261  elp6  4263  opksnelsik  4265  opkelimagekg  4271  elimaksn  4283  xpkvexg  4285  cnvkexg  4286  p6exg  4290  sikexg  4296  dfimak2  4298  ins2kexg  4305  ins3kexg  4306  setswith  4321  ndisjrelk  4323  dfpw2  4327  eqpw1uni  4330  dfaddc2  4381  dfnnc2  4395  peano2  4403  nncaddccl  4419  nnsucelrlem1  4424  nnsucelr  4428  preaddccan2lem1  4454  leltfintr  4458  ltfinex  4464  ltfintrilem1  4465  ltfintri  4466  lenltfin  4469  ssfin  4470  eqpwrelk  4478  eqpw1relk  4479  ncfinraiselem2  4480  ncfinraise  4481  ncfinlowerlem1  4482  ncfinlower  4483  nnpw1ex  4484  eqtfinrelk  4486  tfincl  4492  tfindi  4496  tfinsuc  4498  tfinltfin  4501  evenfinex  4503  oddfinex  4504  evenodddisjlem1  4515  eventfin  4517  oddtfin  4518  nnadjoinlem1  4519  nnadjoin  4520  nnpweqlem1  4522  nnpweq  4523  srelk  4524  sfin01  4528  sfindbl  4530  sfintfinlem1  4531  tfinnnlem1  4533  tfinnn  4534  sfinltfin  4535  spfinex  4537  1cvsfin  4542  vfintle  4546  vfinncvntnn  4548  vfinspsslem1  4550  vfinspss  4551  vfinspclt  4552  vfinncsp  4554  dfop2lem1  4573  proj1op  4600  proj2op  4601  opeq  4619  breq1  4642  breq2  4643  opelopabsb  4697  setconslem1  4731  setconslem2  4732  setconslem3  4733  setconslem4  4734  setconslem6  4736  setconslem7  4737  df1st2  4738  dfswap2  4741  dfima2  4745  dfco1  4748  dfsi2  4751  opeliunxp2  4822  ssrel  4844  ssopr  4846  opabid2  4861  opeldm  4910  elimapw12  4945  elimapw13  4946  elimapw11c  4948  elsnres  4996  iss  5000  xpexr  5109  nfunv  5138  ndmfvrcl  5350  respreima  5410  fvelrn  5413  ffnfvf  5428  ffvresb  5431  fsn  5432  fressnfv  5439  funfvima  5459  ffnov  5587  fovcl  5588  funimassov  5609  ndmovcl  5614  ndmovrcl  5616  caovcld  5622  oprabid2  5646  fvmpti  5699  ov2gf  5711  ovmpt2x  5712  fvmptf  5722  fvmptss2  5725  fmpt2x  5730  otelins2  5791  otelins3  5792  oqelins4  5794  txpcofun  5803  clos1exg  5877  mapex  6006  bren  6030  xpassen  6057  ce0nnul  6177  ce0nnuli  6178  ce0addcnnul  6179  cenc  6181  ce0nulnc  6184  fce  6188  ce0tb  6238  ncfin  6247  addccan2nclem2  6264  nchoicelem6  6294  nchoicelem11  6299  nchoicelem12  6300  nchoicelem16  6304  nchoicelem17  6305  nchoicelem18  6306  nchoicelem19  6307  elscan  6330
  Copyright terms: Public domain W3C validator