Theorem nfel1 2913

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

Syntax hints:  Ⅎwnf 1784   ∈ wcel 2113  Ⅎwnfc 2881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-nf 1785  df-cleq 2726  df-clel 2809  df-nfc 2883

This theorem is referenced by:  vtocl2gf  3525  vtocl3gf  3526  vtoclgaf  3529  vtocl2gaf  3532  vtocl2gafOLD  3533  vtocl3gaf  3534  vtocl3gafOLD  3535  nfop  4843  reusv2lem4  5344  reusv2  5346  rabxfrd  5360  pofun  5548  nfse  5596  fvmptf  6960  fmptcof  7073  fliftfuns  7258  riota2f  7337  ovmpos  7504  ov2gf  7505  elovmporab  7602  elovmporab1w  7603  elovmporab1  7604  ofmpteq  7643  fmpox  8009  offval22  8028  fvmpocurryd  8211  qliftfuns  8739  xpf1o  9065  iunfi  9241  wdom2d  9483  scottex  9795  dfac8clem  9940  ac6num  10387  pwfseqlem4a  10570  pwfseqlem4  10571  gruiin  10719  rlimcld2  15499  summolem3  15635  summolem2a  15636  zsum  15639  fsum  15641  sumss2  15647  fsumcvg2  15648  fsumclf  15659  fsumsplitf  15663  fsum2dlem  15691  fsumcom2  15695  fsumshftm  15702  fsum0diag2  15704  fsum00  15719  fsumabs  15722  fsumrlim  15732  fsumo1  15733  o1fsum  15734  fsumiun  15742  prodmolem3  15854  prodmolem2a  15855  zprod  15858  fprod  15862  prodss  15868  fprodser  15870  fprodm1s  15891  fprodp1s  15892  fprodabs  15895  fprodn0  15900  fprod2dlem  15901  fprodcom2  15905  fproddivf  15908  fprodsplitf  15909  fprodsplit1f  15911  fprodefsum  16016  pcmpt  16818  pcmptdvds  16820  gsumsnf  19880  gsumply1eq  22251  mdetralt2  22551  mdetunilem2  22555  fiuncmp  23346  elptr2  23516  ptcld  23555  ptcnplem  23563  ptcnp  23564  elmptrab  23769  utopsnneiplem  24189  prdsdsf  24309  prdsxmet  24311  fsumcn  24815  ovolfiniun  25456  ovoliunlem3  25459  ovoliun  25460  ovoliun2  25461  finiunmbl  25499  volfiniun  25502  iunmbl  25508  voliun  25509  itgfsum  25782  itgabs  25790  dvmptfsum  25933  dvfsumle  25980  dvfsumleOLD  25981  dvfsumabs  25983  dvfsumlem1  25986  dvfsumlem3  25989  dvfsumlem4  25990  dvfsumrlim  25992  dvfsumrlim2  25993  dvfsum2  25995  itgsubst  26010  fsumdvdscom  27149  fsumvma  27178  dchrisumlema  27453  dchrisumlem2  27455  dchrisumlem3  27456  fsumiunle  32859  locfinreflem  33946  esumcl  34136  esum0  34155  esumcst  34169  esumfsup  34176  esum2d  34199  measiun  34324  voliune  34335  volfiniune  34336  iota5f  35867  weiunse  36611  phpreu  37744  poimirlem25  37785  poimirlem26  37786  poimirlem28  37788  itgabsnc  37829  fsumshftd  39151  riotasv2s  39157  cdlemefs32sn1aw  40613  mzpsubmpt  42927  mzpsubst  42932  eq0rabdioph  42960  eqrabdioph  42961  rabdiophlem2  42986  fphpd  43000  monotuz  43125  monotoddzz  43127  oddcomabszz  43128  flcidc  43354  binomcxplemdvbinom  44536  binomcxplemdvsum  44538  binomcxplemnotnn0  44539  modelaxreplem3  45163  rfcnnnub  45223  disjinfi  45378  supxrleubrnmptf  45637  caucvgbf  45675  cvgcaule  45677  fsummulc1f  45759  fsumnncl  45760  fsumf1of  45762  fsumreclf  45764  fsumlessf  45765  fsumsermpt  45767  fmul01  45768  fmuldfeqlem1  45770  fmuldfeq  45771  fmul01lt1lem1  45772  fmul01lt1lem2  45773  fprodexp  45782  fprodabs2  45783  fprodcnlem  45787  climmulf  45792  climsuse  45796  climrecf  45797  climaddf  45803  0ellimcdiv  45835  climsubmpt  45846  climfveqf  45866  climinf2mpt  45900  climinfmpt  45901  fprodcncf  46086  dvmptmulf  46123  dvmptfprod  46131  iblspltprt  46159  stoweidlem3  46189  stoweidlem19  46205  stoweidlem22  46208  stoweidlem42  46228  fourierdlem31  46324  fourierdlem86  46378  fourierdlem89  46381  fourierdlem91  46383  fourierdlem112  46404  sge0f1o  46568  sge0lempt  46596  sge0iunmpt  46604  sge0ltfirpmpt2  46612  sge0isummpt2  46618  sge0xaddlem2  46620  sge0xadd  46621  vonhoire  46858  salpreimagelt  46893  smflim  46963  smfresal  46974  smfinflem  47003  eu2ndop1stv  47313