Theorem nfel1 2938

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

Step	Hyp	Ref	Expression
1		nfeq1.1	. 2 ⊢ Ⅎ𝑥𝐴
2		nfcv 2922	. 2 ⊢ Ⅎ𝑥𝐵
3	1, 2	nfel 2936	1 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵

This proof depends on syntax axioms:  Ⅎwnf 1816   ∈ wcel 2145  Ⅎwnfc 2907

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-nf 1817  df-cleq 2752  df-clel 2835  df-nfc 2909

This theorem is used by:  vtocl2gf  3531  vtocl3gf  3532  vtoclgaf  3535  vtocl2gaf  3538  vtocl3gaf  3539  nfop  4849  reusv2lem4  5363  reusv2  5365  rabxfrd  5379  pofun  5574  nfse  5622  fvmptf  7004  fmptcof  7120  fliftfuns  7311  riota2f  7390  ovmpos  7557  ov2gf  7558  elovmporab  7656  elovmporab1w  7657  elovmporab1  7658  ofmpteq  7700  fmpox  8062  offval22  8083  fvmpocurryd  8267  qliftfuns  8804  xpf1o  9137  iunfi  9310  wdom2d  9552  scottexOLD  9891  dfac8clem  10068  ac6num  10514  pwfseqlem4a  10703  pwfseqlem4  10704  gruiin  10852  rlimcld2  15698  summolem3  15833  summolem2a  15834  zsum  15837  fsum  15839  sumss2  15845  fsumcvg2  15846  fsumclf  15857  fsumsplitf  15861  fsum2dlem  15889  fsumcom2  15893  fsumshftm  15900  fsum0diag2  15902  fsum00  15918  fsumabs  15921  fsumrlim  15931  fsumo1  15932  o1fsum  15933  fsumiun  15941  prodmolem3  16053  prodmolem2a  16054  zprod  16057  fprod  16061  prodss  16067  fprodser  16069  fprodm1s  16090  fprodp1s  16091  fprodabs  16094  fprodn0  16099  fprod2dlem  16100  fprodcom2  16104  fproddivf  16107  fprodsplitf  16108  fprodsplit1f  16110  fprodefsum  16214  pcmpt  17017  pcmptdvds  17019  gsumsnf  20114  gsumply1eq  22574  mdetralt2  22871  mdetunilem2  22875  fiuncmp  23669  elptr2  23840  ptcld  23879  ptcnplem  23887  ptcnp  23888  elmptrab  24093  utopsnneiplem  24513  prdsdsf  24633  prdsxmet  24635  fsumcn  25138  ovolfiniun  25769  ovoliunlem3  25772  ovoliun  25773  ovoliun2  25774  finiunmbl  25812  volfiniun  25815  iunmbl  25821  voliun  25822  itgfsum  26094  itgabs  26102  dvmptfsum  26242  dvfsumle  26288  dvfsumabs  26290  dvfsumlem1  26293  dvfsumlem3  26295  dvfsumlem4  26296  dvfsumrlim  26298  dvfsumrlim2  26299  dvfsum2  26301  itgsubst  26316  fsumdvdscom  27461  fsumvma  27489  dchrisumlema  27764  dchrisumlem2  27766  dchrisumlem3  27767  fsumiunle  33339  locfinreflem  34391  esumcl  34581  esum0  34600  esumcst  34614  esumfsup  34621  esum2d  34644  measiun  34770  voliune  34781  volfiniune  34782  vonf1oonfo  35813  iota5f  36404  weiunse  37172  phpreu  38441  poimirlem25  38477  poimirlem26  38478  poimirlem28  38480  itgabsnc  38521  fsumshftd  39923  riotasv2s  39929  cdlemefs32sn1aw  41385  mzpsubmpt  43686  mzpsubst  43691  eq0rabdioph  43719  eqrabdioph  43720  rabdiophlem2  43741  fphpd  43755  monotuz  43880  monotoddzz  43882  oddcomabszz  43883  flcidc  44109  binomcxplemdvbinom  45275  binomcxplemdvsum  45277  binomcxplemnotnn0  45278  modelaxreplem3  45901  rfcnnnub  45968  disjinfi  46122  supxrleubrnmptf  46377  caucvgbf  46415  cvgcaule  46417  fsummulc1f  46499  fsumnncl  46500  fsumf1of  46502  fsumreclf  46504  fsumlessf  46505  fsumsermpt  46507  fmul01  46508  fmuldfeqlem1  46510  fmuldfeq  46511  fmul01lt1lem1  46512  fmul01lt1lem2  46513  fprodexp  46522  fprodabs2  46523  fprodcnlem  46527  climmulf  46532  climsuse  46536  climrecf  46537  climaddf  46543  0ellimcdiv  46575  climsubmpt  46586  climfveqf  46606  climinf2mpt  46640  climinfmpt  46641  fprodcncf  46826  dvmptmulf  46863  dvmptfprod  46871  iblspltprt  46899  stoweidlem3  46929  stoweidlem19  46945  stoweidlem22  46948  stoweidlem42  46968  fourierdlem31  47064  fourierdlem86  47118  fourierdlem89  47121  fourierdlem91  47123  fourierdlem112  47144  sge0f1o  47308  sge0lempt  47336  sge0iunmpt  47344  sge0ltfirpmpt2  47352  sge0isummpt2  47358  sge0xaddlem2  47360  sge0xadd  47361  vonhoire  47598  salpreimagelt  47633  smflim  47703  smfresal  47714  smfinflem  47743  eu2ndop1stv  48111