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

Theorem nfel1 2808
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 2793 . 2 𝑥𝐵
31, 2nfel 2806 1 𝑥 𝐴𝐵
Colors of variables: wff setvar class
Syntax hints:  wnf 1748  wcel 2030  wnfc 2780
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-cleq 2644  df-clel 2647  df-nfc 2782
This theorem is referenced by:  vtocl2gf  3299  vtocl3gf  3300  vtoclgaf  3302  vtocl2gaf  3304  vtocl3gaf  3306  nfop  4449  reusv2lem4  4902  reusv2  4904  rabxfrd  4919  pofun  5080  nfse  5118  fvmptf  6340  fmptcof  6437  fliftfuns  6604  riota2f  6672  ovmpt2s  6826  ov2gf  6827  elovmpt2rab  6922  elovmpt2rab1  6923  ofmpteq  6958  fmpt2x  7281  offval22  7298  fvmpt2curryd  7442  qliftfuns  7877  xpf1o  8163  iunfi  8295  wdom2d  8526  scottex  8786  dfac8clem  8893  ac6num  9339  pwfseqlem4a  9521  pwfseqlem4  9522  gruiin  9670  rlimcld2  14353  summolem3  14489  summolem2a  14490  zsum  14493  fsum  14495  sumss2  14501  fsumcvg2  14502  fsumsplitf  14516  fsum2dlem  14545  fsumcom2  14549  fsumcom2OLD  14550  fsumshftm  14557  fsum0diag2  14559  fsum00  14574  fsumabs  14577  fsumrlim  14587  fsumo1  14588  o1fsum  14589  fsumiun  14597  prodmolem3  14707  prodmolem2a  14708  zprod  14711  fprod  14715  prodss  14721  fprodser  14723  fprodm1s  14744  fprodp1s  14745  fprodabs  14748  fprodn0  14753  fprod2dlem  14754  fprodcom2  14758  fprodcom2OLD  14759  fprodsplitf  14763  fprodefsum  14869  pcmpt  15643  pcmptdvds  15645  gsumsnf  18399  gsumply1eq  19723  mdetralt2  20463  mdetunilem2  20467  fiuncmp  21255  elptr2  21425  ptcld  21464  ptcnplem  21472  ptcnp  21473  elmptrab  21678  utopsnneiplem  22098  prdsdsf  22219  prdsxmet  22221  fsumcn  22720  ovolfiniun  23315  ovoliunlem3  23318  ovoliun  23319  ovoliun2  23320  finiunmbl  23358  volfiniun  23361  iunmbl  23367  voliun  23368  itgfsum  23638  itgabs  23646  dvmptfsum  23783  dvfsumle  23829  dvfsumabs  23831  dvfsumlem1  23834  dvfsumlem3  23836  dvfsumlem4  23837  dvfsumrlim  23839  dvfsumrlim2  23840  dvfsum2  23842  itgsubst  23857  fsumdvdscom  24956  fsumvma  24983  dchrisumlema  25222  dchrisumlem2  25224  dchrisumlem3  25225  fsumiunle  29703  locfinreflem  30035  esumcl  30220  esum0  30239  esumcst  30253  esumfsup  30260  esum2d  30283  measiun  30409  voliune  30420  volfiniune  30421  iota5f  31732  phpreu  33523  poimirlem25  33564  poimirlem26  33565  poimirlem28  33567  itgabsnc  33609  fsumshftd  34556  riotasv2s  34562  cdlemefs32sn1aw  36019  mzpsubmpt  37623  mzpsubst  37628  eq0rabdioph  37657  eqrabdioph  37658  rabdiophlem2  37683  fphpd  37697  monotuz  37823  monotoddzz  37825  oddcomabszz  37826  flcidc  38061  binomcxplemdvbinom  38869  binomcxplemdvsum  38871  binomcxplemnotnn0  38872  rfcnnnub  39509  supxrleubrnmptf  39993  fsumclf  40119  fsummulc1f  40120  fsumnncl  40121  fsumf1of  40124  fsumreclf  40126  fsumlessf  40127  fsumsermpt  40129  fmul01  40130  fmuldfeqlem1  40132  fmuldfeq  40133  fmul01lt1lem1  40134  fmul01lt1lem2  40135  fprodexp  40144  fprodabs2  40145  fprodcnlem  40149  climmulf  40154  climsuse  40158  climrecf  40159  climaddf  40165  0ellimcdiv  40199  climsubmpt  40210  climfveqf  40230  climinf2mpt  40264  climinfmpt  40265  fprodcncf  40432  dvmptmulf  40470  iblspltprt  40507  stoweidlem3  40538  stoweidlem19  40554  stoweidlem22  40557  stoweidlem42  40577  fourierdlem31  40673  fourierdlem86  40727  fourierdlem89  40730  fourierdlem91  40732  fourierdlem112  40753  sge0f1o  40917  sge0lempt  40945  sge0iunmpt  40953  sge0ltfirpmpt2  40961  sge0isummpt2  40967  sge0xaddlem2  40969  sge0xadd  40970  vonhoire  41207  salpreimagelt  41239  smflim  41306  smfresal  41316  smfinflem  41344  eu2ndop1stv  41523
  Copyright terms: Public domain W3C validator