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

Theorem nfel1 2922
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 2907 . 2 𝑥𝐵
31, 2nfel 2920 1 𝑥 𝐴𝐵
Colors of variables: wff setvar class
Syntax hints:  wnf 1878  wcel 2155  wnfc 2894
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-cleq 2758  df-clel 2761  df-nfc 2896
This theorem is referenced by:  vtocl2gf  3420  vtocl3gf  3421  vtoclgaf  3423  vtocl2gaf  3425  vtocl3gaf  3427  nfop  4575  reusv2lem4  5036  reusv2  5038  rabxfrd  5052  pofun  5214  nfse  5252  fvmptf  6490  fmptcof  6588  fliftfuns  6756  riota2f  6824  ovmpt2s  6982  ov2gf  6983  elovmpt2rab  7078  elovmpt2rab1  7079  ofmpteq  7114  fmpt2x  7437  offval22  7455  fvmpt2curryd  7600  qliftfuns  8037  xpf1o  8329  iunfi  8461  wdom2d  8692  scottex  8963  dfac8clem  9106  ac6num  9554  pwfseqlem4a  9736  pwfseqlem4  9737  gruiin  9885  rlimcld2  14594  summolem3  14730  summolem2a  14731  zsum  14734  fsum  14736  sumss2  14742  fsumcvg2  14743  fsumsplitf  14757  fsum2dlem  14786  fsumcom2  14790  fsumshftm  14797  fsum0diag2  14799  fsum00  14814  fsumabs  14817  fsumrlim  14827  fsumo1  14828  o1fsum  14829  fsumiun  14837  prodmolem3  14946  prodmolem2a  14947  zprod  14950  fprod  14954  prodss  14960  fprodser  14962  fprodm1s  14983  fprodp1s  14984  fprodabs  14987  fprodn0  14992  fprod2dlem  14993  fprodcom2  14997  fprodsplitf  15001  fprodefsum  15107  pcmpt  15875  pcmptdvds  15877  gsumsnf  18619  gsumply1eq  19948  mdetralt2  20692  mdetunilem2  20696  fiuncmp  21487  elptr2  21657  ptcld  21696  ptcnplem  21704  ptcnp  21705  elmptrab  21910  utopsnneiplem  22330  prdsdsf  22451  prdsxmet  22453  fsumcn  22952  ovolfiniun  23559  ovoliunlem3  23562  ovoliun  23563  ovoliun2  23564  finiunmbl  23602  volfiniun  23605  iunmbl  23611  voliun  23612  itgfsum  23884  itgabs  23892  dvmptfsum  24029  dvfsumle  24075  dvfsumabs  24077  dvfsumlem1  24080  dvfsumlem3  24082  dvfsumlem4  24083  dvfsumrlim  24085  dvfsumrlim2  24086  dvfsum2  24088  itgsubst  24103  fsumdvdscom  25202  fsumvma  25229  dchrisumlema  25468  dchrisumlem2  25470  dchrisumlem3  25471  fsumiunle  30024  locfinreflem  30354  esumcl  30539  esum0  30558  esumcst  30572  esumfsup  30579  esum2d  30602  measiun  30728  voliune  30739  volfiniune  30740  iota5f  32052  phpreu  33817  poimirlem25  33858  poimirlem26  33859  poimirlem28  33861  itgabsnc  33902  fsumshftd  34908  riotasv2s  34914  cdlemefs32sn1aw  36370  mzpsubmpt  37984  mzpsubst  37989  eq0rabdioph  38018  eqrabdioph  38019  rabdiophlem2  38044  fphpd  38058  monotuz  38183  monotoddzz  38185  oddcomabszz  38186  flcidc  38421  binomcxplemdvbinom  39226  binomcxplemdvsum  39228  binomcxplemnotnn0  39229  rfcnnnub  39847  supxrleubrnmptf  40317  fsumclf  40439  fsummulc1f  40440  fsumnncl  40441  fsumf1of  40444  fsumreclf  40446  fsumlessf  40447  fsumsermpt  40449  fmul01  40450  fmuldfeqlem1  40452  fmuldfeq  40453  fmul01lt1lem1  40454  fmul01lt1lem2  40455  fprodexp  40464  fprodabs2  40465  fprodcnlem  40469  climmulf  40474  climsuse  40478  climrecf  40479  climaddf  40485  0ellimcdiv  40519  climsubmpt  40530  climfveqf  40550  climinf2mpt  40584  climinfmpt  40585  fprodcncf  40752  dvmptmulf  40790  iblspltprt  40826  stoweidlem3  40857  stoweidlem19  40873  stoweidlem22  40876  stoweidlem42  40896  fourierdlem31  40992  fourierdlem86  41046  fourierdlem89  41049  fourierdlem91  41051  fourierdlem112  41072  sge0f1o  41236  sge0lempt  41264  sge0iunmpt  41272  sge0ltfirpmpt2  41280  sge0isummpt2  41286  sge0xaddlem2  41288  sge0xadd  41289  vonhoire  41526  salpreimagelt  41558  smflim  41625  smfresal  41635  smfinflem  41663  eu2ndop1stv  41873
  Copyright terms: Public domain W3C validator