Theorem nfel1 2924

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

Syntax hints:  Ⅎwnf 1786   ∈ wcel 2107  Ⅎwnfc 2888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-nf 1787  df-cleq 2731  df-clel 2817  df-nfc 2890

This theorem is referenced by:  vtocl2gf  3509  vtocl3gf  3510  vtoclgaf  3513  vtocl2gaf  3516  vtocl3gaf  3517  nfop  4821  reusv2lem4  5325  reusv2  5327  rabxfrd  5341  pofun  5522  nfse  5565  fvmptf  6905  fmptcof  7011  fliftfuns  7194  riota2f  7266  ovmpos  7430  ov2gf  7431  elovmporab  7524  elovmporab1w  7525  elovmporab1  7526  ofmpteq  7564  fmpox  7916  offval22  7937  fvmpocurryd  8096  qliftfuns  8602  xpf1o  8935  iunfi  9116  wdom2d  9348  scottex  9652  dfac8clem  9797  ac6num  10244  pwfseqlem4a  10426  pwfseqlem4  10427  gruiin  10575  rlimcld2  15296  summolem3  15435  summolem2a  15436  zsum  15439  fsum  15441  sumss2  15447  fsumcvg2  15448  fsumclf  15459  fsumsplitf  15463  fsum2dlem  15491  fsumcom2  15495  fsumshftm  15502  fsum0diag2  15504  fsum00  15519  fsumabs  15522  fsumrlim  15532  fsumo1  15533  o1fsum  15534  fsumiun  15542  prodmolem3  15652  prodmolem2a  15653  zprod  15656  fprod  15660  prodss  15666  fprodser  15668  fprodm1s  15689  fprodp1s  15690  fprodabs  15693  fprodn0  15698  fprod2dlem  15699  fprodcom2  15703  fproddivf  15706  fprodsplitf  15707  fprodsplit1f  15709  fprodefsum  15813  pcmpt  16602  pcmptdvds  16604  gsumsnf  19563  gsumply1eq  21485  mdetralt2  21767  mdetunilem2  21771  fiuncmp  22564  elptr2  22734  ptcld  22773  ptcnplem  22781  ptcnp  22782  elmptrab  22987  utopsnneiplem  23408  prdsdsf  23529  prdsxmet  23531  fsumcn  24042  ovolfiniun  24674  ovoliunlem3  24677  ovoliun  24678  ovoliun2  24679  finiunmbl  24717  volfiniun  24720  iunmbl  24726  voliun  24727  itgfsum  25000  itgabs  25008  dvmptfsum  25148  dvfsumle  25194  dvfsumabs  25196  dvfsumlem1  25199  dvfsumlem3  25201  dvfsumlem4  25202  dvfsumrlim  25204  dvfsumrlim2  25205  dvfsum2  25207  itgsubst  25222  fsumdvdscom  26343  fsumvma  26370  dchrisumlema  26645  dchrisumlem2  26647  dchrisumlem3  26648  fsumiunle  31152  locfinreflem  31799  esumcl  32007  esum0  32026  esumcst  32040  esumfsup  32047  esum2d  32070  measiun  32195  voliune  32206  volfiniune  32207  iota5f  33678  phpreu  35770  poimirlem25  35811  poimirlem26  35812  poimirlem28  35814  itgabsnc  35855  fsumshftd  36973  riotasv2s  36979  cdlemefs32sn1aw  38435  mzpsubmpt  40572  mzpsubst  40577  eq0rabdioph  40605  eqrabdioph  40606  rabdiophlem2  40631  fphpd  40645  monotuz  40770  monotoddzz  40772  oddcomabszz  40773  flcidc  41006  binomcxplemdvbinom  41978  binomcxplemdvsum  41980  binomcxplemnotnn0  41981  rfcnnnub  42586  disjinfi  42738  supxrleubrnmptf  42998  fsummulc1f  43119  fsumnncl  43120  fsumf1of  43122  fsumreclf  43124  fsumlessf  43125  fsumsermpt  43127  fmul01  43128  fmuldfeqlem1  43130  fmuldfeq  43131  fmul01lt1lem1  43132  fmul01lt1lem2  43133  fprodexp  43142  fprodabs2  43143  fprodcnlem  43147  climmulf  43152  climsuse  43156  climrecf  43157  climaddf  43163  0ellimcdiv  43197  climsubmpt  43208  climfveqf  43228  climinf2mpt  43262  climinfmpt  43263  fprodcncf  43448  dvmptmulf  43485  iblspltprt  43521  stoweidlem3  43551  stoweidlem19  43567  stoweidlem22  43570  stoweidlem42  43590  fourierdlem31  43686  fourierdlem86  43740  fourierdlem89  43743  fourierdlem91  43745  fourierdlem112  43766  sge0f1o  43927  sge0lempt  43955  sge0iunmpt  43963  sge0ltfirpmpt2  43971  sge0isummpt2  43977  sge0xaddlem2  43979  sge0xadd  43980  vonhoire  44217  salpreimagelt  44252  smflim  44322  smfresal  44333  smfinflem  44361  eu2ndop1stv  44628