Theorem nfel1 2942

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

This proof depends on syntax axioms:  Ⅎwnf 1816   ∈ wcel 2147  Ⅎwnfc 2911

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735

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 2755  df-clel 2839  df-nfc 2913

This theorem is used by:  vtocl2gf  3535  vtocl3gf  3536  vtoclgaf  3539  vtocl2gaf  3542  vtocl3gaf  3543  nfop  4852  reusv2lem4  5367  reusv2  5369  rabxfrd  5383  pofun  5581  nfse  5629  fvmptf  7038  fmptcof  7155  fliftfuns  7345  riota2f  7424  ovmpos  7592  ov2gf  7593  elovmporab  7691  elovmporab1w  7692  elovmporab1  7693  ofmpteq  7740  fmpox  8103  offval22  8124  fvmpocurryd  8316  qliftfuns  8853  xpf1o  9186  iunfi  9360  wdom2d  9601  scottexOLD  9961  dfac8clem  10138  ac6num  10584  pwfseqlem4a  10773  pwfseqlem4  10774  gruiin  10922  rlimcld2  15774  summolem3  15909  summolem2a  15910  zsum  15913  fsum  15915  sumss2  15921  fsumcvg2  15922  fsumclf  15933  fsumsplitf  15937  fsum2dlem  15965  fsumcom2  15969  fsumshftm  15976  fsum0diag2  15978  fsum00  15994  fsumabs  15997  fsumrlim  16007  fsumo1  16008  o1fsum  16009  fsumiun  16017  prodmolem3  16129  prodmolem2a  16130  zprod  16133  fprod  16137  prodss  16143  fprodser  16145  fprodm1s  16166  fprodp1s  16167  fprodabs  16170  fprodn0  16175  fprod2dlem  16176  fprodcom2  16180  fproddivf  16183  fprodsplitf  16184  fprodsplit1f  16186  fprodefsum  16290  pcmpt  17099  pcmptdvds  17101  gsumsnf  20197  gsumply1eq  22657  mdetralt2  22954  mdetunilem2  22958  fiuncmp  23752  elptr2  23923  ptcld  23962  ptcnplem  23970  ptcnp  23971  elmptrab  24176  utopsnneiplem  24596  prdsdsf  24716  prdsxmet  24718  fsumcn  25221  ovolfiniun  25852  ovoliunlem3  25855  ovoliun  25856  ovoliun2  25857  finiunmbl  25895  volfiniun  25898  iunmbl  25904  voliun  25905  itgfsum  26177  itgabs  26185  dvmptfsum  26325  dvfsumle  26371  dvfsumabs  26373  dvfsumlem1  26376  dvfsumlem3  26378  dvfsumlem4  26379  dvfsumrlim  26381  dvfsumrlim2  26382  dvfsum2  26384  itgsubst  26399  fsumdvdscom  27542  fsumvma  27570  dchrisumlema  27845  dchrisumlem2  27847  dchrisumlem3  27848  fsumiunle  33490  locfinreflem  34542  esumcl  34732  esum0  34751  esumcst  34765  esumfsup  34772  esum2d  34795  measiun  34921  voliune  34932  volfiniune  34933  omssubadd  35002  rankse  35823  vonf1oonfo  36049  iota5f  36667  weiunse  37434  phpreu  38719  poimirlem25  38755  poimirlem26  38756  poimirlem28  38758  itgabsnc  38799  fsumshftd  40201  riotasv2s  40207  cdlemefs32sn1aw  41663  mzpsubmpt  43947  mzpsubst  43952  eq0rabdioph  43980  eqrabdioph  43981  rabdiophlem2  44002  fphpd  44016  monotuz  44141  monotoddzz  44143  oddcomabszz  44144  flcidc  44364  binomcxplemdvbinom  45529  binomcxplemdvsum  45531  binomcxplemnotnn0  45532  modelaxreplem3  46165  rfcnnnub  46258  disjinfi  46412  supxrleubrnmptf  46666  caucvgbf  46704  cvgcaule  46706  fsummulc1f  46788  fsumnncl  46789  fsumf1of  46791  fsumreclf  46793  fsumlessf  46794  fsumsermpt  46796  fmul01  46797  fmuldfeqlem1  46799  fmuldfeq  46800  fmul01lt1lem1  46801  fmul01lt1lem2  46802  fprodexp  46811  fprodabs2  46812  fprodcnlem  46816  climmulf  46821  climsuse  46825  climrecf  46826  climaddf  46832  0ellimcdiv  46864  climsubmpt  46875  climfveqf  46895  climinf2mpt  46929  climinfmpt  46930  fprodcncf  47115  dvmptmulf  47152  dvmptfprod  47160  iblspltprt  47188  stoweidlem3  47218  stoweidlem19  47234  stoweidlem22  47237  stoweidlem42  47257  fourierdlem31  47353  fourierdlem86  47407  fourierdlem89  47410  fourierdlem91  47412  fourierdlem112  47433  sge0f1o  47597  sge0lempt  47625  sge0iunmpt  47633  sge0ltfirpmpt2  47641  sge0isummpt2  47647  sge0xaddlem2  47649  sge0xadd  47650  vonhoire  47887  salpreimagelt  47922  smflim  47992  smfresal  48003  smfinflem  48032  eu2ndop1stv  48400