Theorem nfel1 2971

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 2955	. 2 ⊢ Ⅎ𝑥𝐵
3	1, 2	nfel 2969	1 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵

Syntax hints:  Ⅎwnf 1785   ∈ wcel 2111  Ⅎwnfc 2936

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-cleq 2791  df-clel 2870  df-nfc 2938

This theorem is referenced by:  vtocl2gf  3518  vtocl3gf  3519  vtoclgaf  3521  vtocl2gaf  3524  vtocl3gaf  3525  nfop  4781  reusv2lem4  5267  reusv2  5269  rabxfrd  5283  pofun  5455  nfse  5494  fvmptf  6766  fmptcof  6869  fliftfuns  7046  riota2f  7117  ovmpos  7277  ov2gf  7278  elovmporab  7371  elovmporab1w  7372  elovmporab1  7373  ofmpteq  7408  fmpox  7747  offval22  7766  fvmpocurryd  7920  qliftfuns  8367  xpf1o  8663  iunfi  8796  wdom2d  9028  scottex  9298  dfac8clem  9443  ac6num  9890  pwfseqlem4a  10072  pwfseqlem4  10073  gruiin  10221  rlimcld2  14927  summolem3  15063  summolem2a  15064  zsum  15067  fsum  15069  sumss2  15075  fsumcvg2  15076  fsumsplitf  15090  fsum2dlem  15117  fsumcom2  15121  fsumshftm  15128  fsum0diag2  15130  fsum00  15145  fsumabs  15148  fsumrlim  15158  fsumo1  15159  o1fsum  15160  fsumiun  15168  prodmolem3  15279  prodmolem2a  15280  zprod  15283  fprod  15287  prodss  15293  fprodser  15295  fprodm1s  15316  fprodp1s  15317  fprodabs  15320  fprodn0  15325  fprod2dlem  15326  fprodcom2  15330  fproddivf  15333  fprodsplitf  15334  fprodsplit1f  15336  fprodefsum  15440  pcmpt  16218  pcmptdvds  16220  gsumsnf  19066  gsumply1eq  20934  mdetralt2  21214  mdetunilem2  21218  fiuncmp  22009  elptr2  22179  ptcld  22218  ptcnplem  22226  ptcnp  22227  elmptrab  22432  utopsnneiplem  22853  prdsdsf  22974  prdsxmet  22976  fsumcn  23475  ovolfiniun  24105  ovoliunlem3  24108  ovoliun  24109  ovoliun2  24110  finiunmbl  24148  volfiniun  24151  iunmbl  24157  voliun  24158  itgfsum  24430  itgabs  24438  dvmptfsum  24578  dvfsumle  24624  dvfsumabs  24626  dvfsumlem1  24629  dvfsumlem3  24631  dvfsumlem4  24632  dvfsumrlim  24634  dvfsumrlim2  24635  dvfsum2  24637  itgsubst  24652  fsumdvdscom  25770  fsumvma  25797  dchrisumlema  26072  dchrisumlem2  26074  dchrisumlem3  26075  fsumiunle  30571  locfinreflem  31193  esumcl  31399  esum0  31418  esumcst  31432  esumfsup  31439  esum2d  31462  measiun  31587  voliune  31598  volfiniune  31599  iota5f  33068  phpreu  35041  poimirlem25  35082  poimirlem26  35083  poimirlem28  35085  itgabsnc  35126  fsumshftd  36248  riotasv2s  36254  cdlemefs32sn1aw  37710  mzpsubmpt  39684  mzpsubst  39689  eq0rabdioph  39717  eqrabdioph  39718  rabdiophlem2  39743  fphpd  39757  monotuz  39882  monotoddzz  39884  oddcomabszz  39885  flcidc  40118  binomcxplemdvbinom  41057  binomcxplemdvsum  41059  binomcxplemnotnn0  41060  rfcnnnub  41665  disjinfi  41820  supxrleubrnmptf  42090  fsumclf  42211  fsummulc1f  42212  fsumnncl  42213  fsumf1of  42216  fsumreclf  42218  fsumlessf  42219  fsumsermpt  42221  fmul01  42222  fmuldfeqlem1  42224  fmuldfeq  42225  fmul01lt1lem1  42226  fmul01lt1lem2  42227  fprodexp  42236  fprodabs2  42237  fprodcnlem  42241  climmulf  42246  climsuse  42250  climrecf  42251  climaddf  42257  0ellimcdiv  42291  climsubmpt  42302  climfveqf  42322  climinf2mpt  42356  climinfmpt  42357  fprodcncf  42542  dvmptmulf  42579  iblspltprt  42615  stoweidlem3  42645  stoweidlem19  42661  stoweidlem22  42664  stoweidlem42  42684  fourierdlem31  42780  fourierdlem86  42834  fourierdlem89  42837  fourierdlem91  42839  fourierdlem112  42860  sge0f1o  43021  sge0lempt  43049  sge0iunmpt  43057  sge0ltfirpmpt2  43065  sge0isummpt2  43071  sge0xaddlem2  43073  sge0xadd  43074  vonhoire  43311  salpreimagelt  43343  smflim  43410  smfresal  43420  smfinflem  43448  eu2ndop1stv  43681