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

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

Proof of Theorem eleq1d
StepHypRef Expression
1 eleq1d.1 . 2
2 eleq1 2413 . 2
31, 2syl 15 1
Colors of variables: wff set class
Syntax hints:   wi 4   wb 176   wceq 1642   wcel 1710
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  4418  nnsucelrlem1  4423  nnsucelr  4427  preaddccan1lem1  4453  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  4598  proj2op  4599  breq1  4634  breq2  4635  opelopabsb  4689  setconslem1  4723  setconslem2  4724  setconslem3  4725  setconslem4  4726  setconslem6  4728  setconslem7  4729  df1st2  4730  dfswap2  4733  dfima2  4737  dfco1  4740  dfsi2  4743  opabid2  4874  opeldm  4922  elreldm  4941  elimapw12  4959  elimapw13  4960  elimapw11c  4962  elsnres  5011  iss  5015  xpexr  5142  ndmfvrcl  5390  respreima  5450  fvelrn  5453  ffnfvf  5468  ffvresb  5471  fsn  5472  fressnfv  5479  funfvima  5499  ffnov  5629  fovcl  5630  funimassov  5651  ndmovcl  5656  ndmovrcl  5658  caovcld  5664  fvmpti  5739  ov2gf  5750  ovmpt2x  5751  fvmptf  5762  fvmptss2  5765  otelins2  5820  otelins3  5821  oqelins4  5823  clos1exg  5899  refex  5931  antisymex  5932  connexex  5933  mapex  6026  bren  6051  enmap2lem1  6083  enmap1lem1  6089  ce0nnul  6198  ce0nnuli  6199  ce0addcnnul  6200  cenc  6202  ce0nulnc  6205  fce  6209  ce0tb  6258  ncfin  6267  nchoicelem6  6294  nchoicelem11  6299  nchoicelem12  6300  nchoicelem16  6304  nchoicelem17  6305  nchoicelem18  6306  nchoicelem19  6307
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 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
  Copyright terms: Public domain W3C validator