MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfel1 Structured version   Visualization version   GIF version

Theorem nfel1 2924
Description: Hypothesis builder for elementhood, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
Hypothesis
Ref Expression
nfeq1.1 𝑥𝐴
Assertion
Ref Expression
nfel1 𝑥 𝐴𝐵
Distinct variable group:   𝑥,𝐵
Allowed substitution hint:   𝐴(𝑥)

Proof of Theorem nfel1
StepHypRef Expression
1 nfeq1.1 . 2 𝑥𝐴
2 nfcv 2908 . 2 𝑥𝐵
31, 2nfel 2922 1 𝑥 𝐴𝐵
Colors of variables: wff setvar class
Syntax hints:  wnf 1786  wcel 2107  wnfc 2888
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-nf 1787  df-cleq 2729  df-clel 2815  df-nfc 2890
This theorem is referenced by:  vtocl2gf  3532  vtocl3gf  3533  vtoclgaf  3536  vtocl2gaf  3539  vtocl3gaf  3540  nfop  4851  reusv2lem4  5361  reusv2  5363  rabxfrd  5377  pofun  5568  nfse  5613  fvmptf  6974  fmptcof  7081  fliftfuns  7264  riota2f  7343  ovmpos  7508  ov2gf  7509  elovmporab  7604  elovmporab1w  7605  elovmporab1  7606  ofmpteq  7644  fmpox  8004  offval22  8025  fvmpocurryd  8207  qliftfuns  8750  xpf1o  9090  iunfi  9291  wdom2d  9523  scottex  9828  dfac8clem  9975  ac6num  10422  pwfseqlem4a  10604  pwfseqlem4  10605  gruiin  10753  rlimcld2  15467  summolem3  15606  summolem2a  15607  zsum  15610  fsum  15612  sumss2  15618  fsumcvg2  15619  fsumclf  15630  fsumsplitf  15634  fsum2dlem  15662  fsumcom2  15666  fsumshftm  15673  fsum0diag2  15675  fsum00  15690  fsumabs  15693  fsumrlim  15703  fsumo1  15704  o1fsum  15705  fsumiun  15713  prodmolem3  15823  prodmolem2a  15824  zprod  15827  fprod  15831  prodss  15837  fprodser  15839  fprodm1s  15860  fprodp1s  15861  fprodabs  15864  fprodn0  15869  fprod2dlem  15870  fprodcom2  15874  fproddivf  15877  fprodsplitf  15878  fprodsplit1f  15880  fprodefsum  15984  pcmpt  16771  pcmptdvds  16773  gsumsnf  19737  gsumply1eq  21692  mdetralt2  21974  mdetunilem2  21978  fiuncmp  22771  elptr2  22941  ptcld  22980  ptcnplem  22988  ptcnp  22989  elmptrab  23194  utopsnneiplem  23615  prdsdsf  23736  prdsxmet  23738  fsumcn  24249  ovolfiniun  24881  ovoliunlem3  24884  ovoliun  24885  ovoliun2  24886  finiunmbl  24924  volfiniun  24927  iunmbl  24933  voliun  24934  itgfsum  25207  itgabs  25215  dvmptfsum  25355  dvfsumle  25401  dvfsumabs  25403  dvfsumlem1  25406  dvfsumlem3  25408  dvfsumlem4  25409  dvfsumrlim  25411  dvfsumrlim2  25412  dvfsum2  25414  itgsubst  25429  fsumdvdscom  26550  fsumvma  26577  dchrisumlema  26852  dchrisumlem2  26854  dchrisumlem3  26855  fsumiunle  31767  locfinreflem  32461  esumcl  32669  esum0  32688  esumcst  32702  esumfsup  32709  esum2d  32732  measiun  32857  voliune  32868  volfiniune  32869  iota5f  34335  phpreu  36091  poimirlem25  36132  poimirlem26  36133  poimirlem28  36135  itgabsnc  36176  fsumshftd  37443  riotasv2s  37449  cdlemefs32sn1aw  38906  mzpsubmpt  41095  mzpsubst  41100  eq0rabdioph  41128  eqrabdioph  41129  rabdiophlem2  41154  fphpd  41168  monotuz  41294  monotoddzz  41296  oddcomabszz  41297  flcidc  41530  binomcxplemdvbinom  42707  binomcxplemdvsum  42709  binomcxplemnotnn0  42710  rfcnnnub  43315  disjinfi  43486  supxrleubrnmptf  43760  caucvgbf  43799  cvgcaule  43801  fsummulc1f  43886  fsumnncl  43887  fsumf1of  43889  fsumreclf  43891  fsumlessf  43892  fsumsermpt  43894  fmul01  43895  fmuldfeqlem1  43897  fmuldfeq  43898  fmul01lt1lem1  43899  fmul01lt1lem2  43900  fprodexp  43909  fprodabs2  43910  fprodcnlem  43914  climmulf  43919  climsuse  43923  climrecf  43924  climaddf  43930  0ellimcdiv  43964  climsubmpt  43975  climfveqf  43995  climinf2mpt  44029  climinfmpt  44030  fprodcncf  44215  dvmptmulf  44252  iblspltprt  44288  stoweidlem3  44318  stoweidlem19  44334  stoweidlem22  44337  stoweidlem42  44357  fourierdlem31  44453  fourierdlem86  44507  fourierdlem89  44510  fourierdlem91  44512  fourierdlem112  44533  sge0f1o  44697  sge0lempt  44725  sge0iunmpt  44733  sge0ltfirpmpt2  44741  sge0isummpt2  44747  sge0xaddlem2  44749  sge0xadd  44750  vonhoire  44987  salpreimagelt  45022  smflim  45092  smfresal  45103  smfinflem  45132  eu2ndop1stv  45431
  Copyright terms: Public domain W3C validator