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

Theorem nfel1 2765
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 2751 . 2 𝑥𝐵
31, 2nfel 2763 1 𝑥 𝐴𝐵
Colors of variables: wff setvar class
Syntax hints:  wnf 1699  wcel 1977  wnfc 2738
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-cleq 2603  df-clel 2606  df-nfc 2740
This theorem is referenced by:  vtocl2gf  3241  vtocl3gf  3242  vtoclgaf  3244  vtocl2gaf  3246  vtocl3gaf  3248  nfop  4356  reusv2lem4  4798  reusv2  4800  rabxfrd  4815  pofun  4975  nfse  5013  fvmptf  6209  fmptcof  6304  fliftfuns  6464  riota2f  6532  ovmpt2s  6682  ov2gf  6683  elovmpt2rab  6778  elovmpt2rab1  6779  ofmpteq  6814  fmpt2x  7125  offval22  7140  fvmpt2curryd  7284  qliftfuns  7721  xpf1o  8007  iunfi  8137  wdom2d  8368  scottex  8631  dfac8clem  8738  ac6num  9184  pwfseqlem4a  9362  pwfseqlem4  9363  gruiin  9511  rlimcld2  14157  summolem3  14292  summolem2a  14293  zsum  14296  fsum  14298  sumss2  14304  fsumcvg2  14305  fsum2dlem  14343  fsumcom2  14347  fsumcom2OLD  14348  fsumshftm  14355  fsum0diag2  14357  fsum00  14371  fsumabs  14374  fsumrlim  14384  fsumo1  14385  o1fsum  14386  fsumiun  14394  prodmolem3  14502  prodmolem2a  14503  zprod  14506  fprod  14510  prodss  14516  fprodser  14518  fprodm1s  14539  fprodp1s  14540  fprodabs  14543  fprodn0  14548  fprod2dlem  14549  fprodcom2  14553  fprodcom2OLD  14554  fprodsplitf  14558  fprodefsum  14664  pcmpt  15434  pcmptdvds  15436  gsumsnf  18176  gsumply1eq  19496  mdetralt2  20234  mdetunilem2  20238  fiuncmp  21017  elptr2  21187  ptcld  21226  ptcnplem  21234  ptcnp  21235  elmptrab  21440  utopsnneiplem  21861  prdsdsf  21982  prdsxmet  21984  fsumcn  22481  ovolfiniun  23076  ovoliunlem3  23079  ovoliun  23080  ovoliun2  23081  finiunmbl  23119  volfiniun  23122  iunmbl  23128  voliun  23129  itgfsum  23399  itgabs  23407  dvmptfsum  23542  dvfsumle  23588  dvfsumabs  23590  dvfsumlem1  23593  dvfsumlem3  23595  dvfsumlem4  23596  dvfsumrlim  23598  dvfsumrlim2  23599  dvfsum2  23601  itgsubst  23616  fsumdvdscom  24711  fsumvma  24738  dchrisumlema  24977  dchrisumlem2  24979  dchrisumlem3  24980  locfinreflem  29235  esumcl  29419  esum0  29438  esumcst  29452  esumfsup  29459  esum2d  29482  measiun  29608  voliune  29619  volfiniune  29620  iota5f  30861  phpreu  32563  poimirlem25  32604  poimirlem26  32605  poimirlem28  32607  itgabsnc  32649  fsumshftd  33255  fsumshftdOLD  33256  riotasv2s  33262  cdlemefs32sn1aw  34720  mzpsubmpt  36324  mzpsubst  36329  eq0rabdioph  36358  eqrabdioph  36359  rabdiophlem2  36384  fphpd  36398  monotuz  36524  monotoddzz  36526  oddcomabszz  36527  flcidc  36763  binomcxplemdvbinom  37574  binomcxplemdvsum  37576  binomcxplemnotnn0  37577  rfcnnnub  38218  fsumclf  38633  fsumsplitf  38634  fsummulc1f  38635  fsumnncl  38638  fsumf1of  38641  fsumreclf  38643  fsumlessf  38644  fsumsermpt  38646  fmul01  38647  fmuldfeqlem1  38649  fmuldfeq  38650  fmul01lt1lem1  38651  fmul01lt1lem2  38652  fprodexp  38661  fprodabs2  38662  fprodcnlem  38666  climmulf  38671  climsuse  38675  climrecf  38676  climaddf  38682  0ellimcdiv  38716  climsubmpt  38727  fprodcncf  38787  dvmptmulf  38827  iblspltprt  38865  stoweidlem3  38896  stoweidlem19  38912  stoweidlem22  38915  stoweidlem42  38935  fourierdlem31  39031  fourierdlem86  39085  fourierdlem89  39088  fourierdlem91  39090  fourierdlem112  39111  sge0f1o  39275  sge0lempt  39303  sge0iunmpt  39311  sge0ltfirpmpt2  39319  sge0isummpt2  39325  sge0xaddlem2  39327  sge0xadd  39328  vonhoire  39563  salpreimagelt  39595  smflim  39663  smfresal  39673  eu2ndop1stv  39851
  Copyright terms: Public domain W3C validator