Theorem nfel1 2984

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

Syntax hints:  Ⅎwnf 1884   ∈ wcel 2166  Ⅎwnfc 2956

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-tru 1662  df-ex 1881  df-nf 1885  df-cleq 2818  df-clel 2821  df-nfc 2958

This theorem is referenced by:  vtocl2gf  3484  vtocl3gf  3485  vtoclgaf  3488  vtocl2gaf  3490  vtocl3gaf  3492  nfop  4639  reusv2lem4  5101  reusv2  5103  rabxfrd  5117  pofun  5279  nfse  5317  fvmptf  6548  fmptcof  6647  fliftfuns  6819  riota2f  6887  ovmpt2s  7044  ov2gf  7045  elovmpt2rab  7140  elovmpt2rab1  7141  ofmpteq  7176  fmpt2x  7499  offval22  7517  fvmpt2curryd  7662  qliftfuns  8099  xpf1o  8391  iunfi  8523  wdom2d  8754  scottex  9025  dfac8clem  9168  ac6num  9616  pwfseqlem4a  9798  pwfseqlem4  9799  gruiin  9947  rlimcld2  14686  summolem3  14822  summolem2a  14823  zsum  14826  fsum  14828  sumss2  14834  fsumcvg2  14835  fsumsplitf  14849  fsum2dlem  14876  fsumcom2  14880  fsumshftm  14887  fsum0diag2  14889  fsum00  14904  fsumabs  14907  fsumrlim  14917  fsumo1  14918  o1fsum  14919  fsumiun  14927  prodmolem3  15036  prodmolem2a  15037  zprod  15040  fprod  15044  prodss  15050  fprodser  15052  fprodm1s  15073  fprodp1s  15074  fprodabs  15077  fprodn0  15082  fprod2dlem  15083  fprodcom2  15087  fprodsplitf  15091  fprodefsum  15197  pcmpt  15967  pcmptdvds  15969  gsumsnf  18706  gsumply1eq  20035  mdetralt2  20783  mdetunilem2  20787  fiuncmp  21578  elptr2  21748  ptcld  21787  ptcnplem  21795  ptcnp  21796  elmptrab  22001  utopsnneiplem  22421  prdsdsf  22542  prdsxmet  22544  fsumcn  23043  ovolfiniun  23667  ovoliunlem3  23670  ovoliun  23671  ovoliun2  23672  finiunmbl  23710  volfiniun  23713  iunmbl  23719  voliun  23720  itgfsum  23992  itgabs  24000  dvmptfsum  24137  dvfsumle  24183  dvfsumabs  24185  dvfsumlem1  24188  dvfsumlem3  24190  dvfsumlem4  24191  dvfsumrlim  24193  dvfsumrlim2  24194  dvfsum2  24196  itgsubst  24211  fsumdvdscom  25324  fsumvma  25351  dchrisumlema  25590  dchrisumlem2  25592  dchrisumlem3  25593  fsumiunle  30122  locfinreflem  30452  esumcl  30637  esum0  30656  esumcst  30670  esumfsup  30677  esum2d  30700  measiun  30826  voliune  30837  volfiniune  30838  iota5f  32150  phpreu  33936  poimirlem25  33978  poimirlem26  33979  poimirlem28  33981  itgabsnc  34022  fsumshftd  35027  riotasv2s  35033  cdlemefs32sn1aw  36489  mzpsubmpt  38150  mzpsubst  38155  eq0rabdioph  38184  eqrabdioph  38185  rabdiophlem2  38210  fphpd  38224  monotuz  38349  monotoddzz  38351  oddcomabszz  38352  flcidc  38587  binomcxplemdvbinom  39392  binomcxplemdvsum  39394  binomcxplemnotnn0  39395  rfcnnnub  40013  supxrleubrnmptf  40475  fsumclf  40596  fsummulc1f  40597  fsumnncl  40598  fsumf1of  40601  fsumreclf  40603  fsumlessf  40604  fsumsermpt  40606  fmul01  40607  fmuldfeqlem1  40609  fmuldfeq  40610  fmul01lt1lem1  40611  fmul01lt1lem2  40612  fprodexp  40621  fprodabs2  40622  fprodcnlem  40626  climmulf  40631  climsuse  40635  climrecf  40636  climaddf  40642  0ellimcdiv  40676  climsubmpt  40687  climfveqf  40707  climinf2mpt  40741  climinfmpt  40742  fprodcncf  40909  dvmptmulf  40947  iblspltprt  40983  stoweidlem3  41014  stoweidlem19  41030  stoweidlem22  41033  stoweidlem42  41053  fourierdlem31  41149  fourierdlem86  41203  fourierdlem89  41206  fourierdlem91  41208  fourierdlem112  41229  sge0f1o  41390  sge0lempt  41418  sge0iunmpt  41426  sge0ltfirpmpt2  41434  sge0isummpt2  41440  sge0xaddlem2  41442  sge0xadd  41443  vonhoire  41680  salpreimagelt  41712  smflim  41779  smfresal  41789  smfinflem  41817  eu2ndop1stv  42027