Theorem nfel1 2940

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

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

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 2215  ax-ext 2734

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 2754  df-clel 2837  df-nfc 2911

This theorem is used by:  vtocl2gf  3534  vtocl3gf  3535  vtoclgaf  3538  vtocl2gaf  3541  vtocl3gaf  3542  nfop  4852  reusv2lem4  5370  reusv2  5372  rabxfrd  5386  pofun  5585  nfse  5633  fvmptf  7012  fmptcof  7127  fliftfuns  7318  riota2f  7397  ovmpos  7564  ov2gf  7565  elovmporab  7663  elovmporab1w  7664  elovmporab1  7665  ofmpteq  7704  fmpox  8067  offval22  8088  fvmpocurryd  8272  qliftfuns  8807  xpf1o  9140  iunfi  9313  wdom2d  9555  scottexOLD  9876  dfac8clem  10038  ac6num  10484  pwfseqlem4a  10673  pwfseqlem4  10674  gruiin  10822  rlimcld2  15667  summolem3  15802  summolem2a  15803  zsum  15806  fsum  15808  sumss2  15814  fsumcvg2  15815  fsumclf  15826  fsumsplitf  15830  fsum2dlem  15858  fsumcom2  15862  fsumshftm  15869  fsum0diag2  15871  fsum00  15887  fsumabs  15890  fsumrlim  15900  fsumo1  15901  o1fsum  15902  fsumiun  15910  prodmolem3  16024  prodmolem2a  16025  zprod  16028  fprod  16032  prodss  16038  fprodser  16040  fprodm1s  16061  fprodp1s  16062  fprodabs  16065  fprodn0  16070  fprod2dlem  16071  fprodcom2  16075  fproddivf  16078  fprodsplitf  16079  fprodsplit1f  16081  fprodefsum  16185  pcmpt  16988  pcmptdvds  16990  gsumsnf  20081  gsumply1eq  22535  mdetralt2  22832  mdetunilem2  22836  fiuncmp  23630  elptr2  23801  ptcld  23840  ptcnplem  23848  ptcnp  23849  elmptrab  24054  utopsnneiplem  24474  prdsdsf  24594  prdsxmet  24596  fsumcn  25099  ovolfiniun  25730  ovoliunlem3  25733  ovoliun  25734  ovoliun2  25735  finiunmbl  25773  volfiniun  25776  iunmbl  25782  voliun  25783  itgfsum  26056  itgabs  26064  dvmptfsum  26204  dvfsumle  26250  dvfsumabs  26252  dvfsumlem1  26255  dvfsumlem3  26257  dvfsumlem4  26258  dvfsumrlim  26260  dvfsumrlim2  26261  dvfsum2  26263  itgsubst  26278  fsumdvdscom  27419  fsumvma  27447  dchrisumlema  27722  dchrisumlem2  27724  dchrisumlem3  27725  fsumiunle  33286  locfinreflem  34337  esumcl  34527  esum0  34546  esumcst  34560  esumfsup  34567  esum2d  34590  measiun  34716  voliune  34727  volfiniune  34728  vonf1oonfo  35699  iota5f  36290  weiunse  37074  phpreu  38345  poimirlem25  38381  poimirlem26  38382  poimirlem28  38384  itgabsnc  38425  fsumshftd  39812  riotasv2s  39818  cdlemefs32sn1aw  41274  mzpsubmpt  43575  mzpsubst  43580  eq0rabdioph  43608  eqrabdioph  43609  rabdiophlem2  43630  fphpd  43644  monotuz  43769  monotoddzz  43771  oddcomabszz  43772  flcidc  43998  binomcxplemdvbinom  45164  binomcxplemdvsum  45166  binomcxplemnotnn0  45167  modelaxreplem3  45790  rfcnnnub  45857  disjinfi  46011  supxrleubrnmptf  46266  caucvgbf  46304  cvgcaule  46306  fsummulc1f  46388  fsumnncl  46389  fsumf1of  46391  fsumreclf  46393  fsumlessf  46394  fsumsermpt  46396  fmul01  46397  fmuldfeqlem1  46399  fmuldfeq  46400  fmul01lt1lem1  46401  fmul01lt1lem2  46402  fprodexp  46411  fprodabs2  46412  fprodcnlem  46416  climmulf  46421  climsuse  46425  climrecf  46426  climaddf  46432  0ellimcdiv  46464  climsubmpt  46475  climfveqf  46495  climinf2mpt  46529  climinfmpt  46530  fprodcncf  46715  dvmptmulf  46752  dvmptfprod  46760  iblspltprt  46788  stoweidlem3  46818  stoweidlem19  46834  stoweidlem22  46837  stoweidlem42  46857  fourierdlem31  46953  fourierdlem86  47007  fourierdlem89  47010  fourierdlem91  47012  fourierdlem112  47033  sge0f1o  47197  sge0lempt  47225  sge0iunmpt  47233  sge0ltfirpmpt2  47241  sge0isummpt2  47247  sge0xaddlem2  47249  sge0xadd  47250  vonhoire  47487  salpreimagelt  47522  smflim  47592  smfresal  47603  smfinflem  47632  eu2ndop1stv  48000