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 1812   ∈ wcel 2142  Ⅎwnfc 2909

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1572  df-ex 1809  df-nf 1813  df-cleq 2754  df-clel 2837  df-nfc 2911

This theorem is used by:  vtocl2gf  3535  vtocl3gf  3536  vtoclgaf  3539  vtocl2gaf  3542  vtocl3gaf  3543  nfop  4853  reusv2lem4  5371  reusv2  5373  rabxfrd  5387  pofun  5586  nfse  5634  fvmptf  7011  fmptcof  7126  fliftfuns  7312  riota2f  7393  ovmpos  7560  ov2gf  7561  elovmporab  7658  elovmporab1w  7659  elovmporab1  7660  ofmpteq  7699  fmpox  8062  offval22  8081  fvmpocurryd  8265  qliftfuns  8800  xpf1o  9125  iunfi  9298  wdom2d  9540  scottexOLD  9861  dfac8clem  10023  ac6num  10469  pwfseqlem4a  10652  pwfseqlem4  10653  gruiin  10801  rlimcld2  15636  summolem3  15772  summolem2a  15773  zsum  15776  fsum  15778  sumss2  15784  fsumcvg2  15785  fsumclf  15796  fsumsplitf  15800  fsum2dlem  15828  fsumcom2  15832  fsumshftm  15839  fsum0diag2  15841  fsum00  15857  fsumabs  15860  fsumrlim  15870  fsumo1  15871  o1fsum  15872  fsumiun  15880  prodmolem3  15994  prodmolem2a  15995  zprod  15998  fprod  16002  prodss  16008  fprodser  16010  fprodm1s  16031  fprodp1s  16032  fprodabs  16035  fprodn0  16040  fprod2dlem  16041  fprodcom2  16045  fproddivf  16048  fprodsplitf  16049  fprodsplit1f  16051  fprodefsum  16155  pcmpt  16958  pcmptdvds  16960  gsumsnf  20029  gsumply1eq  22480  mdetralt2  22777  mdetunilem2  22781  fiuncmp  23572  elptr2  23742  ptcld  23781  ptcnplem  23789  ptcnp  23790  elmptrab  23995  utopsnneiplem  24415  prdsdsf  24535  prdsxmet  24537  fsumcn  25040  ovolfiniun  25671  ovoliunlem3  25674  ovoliun  25675  ovoliun2  25676  finiunmbl  25714  volfiniun  25717  iunmbl  25723  voliun  25724  itgfsum  25997  itgabs  26005  dvmptfsum  26145  dvfsumle  26191  dvfsumabs  26193  dvfsumlem1  26196  dvfsumlem3  26198  dvfsumlem4  26199  dvfsumrlim  26201  dvfsumrlim2  26202  dvfsum2  26204  itgsubst  26219  fsumdvdscom  27360  fsumvma  27388  dchrisumlema  27663  dchrisumlem2  27665  dchrisumlem3  27666  fsumiunle  33184  locfinreflem  34239  esumcl  34429  esum0  34448  esumcst  34462  esumfsup  34469  esum2d  34492  measiun  34617  voliune  34628  volfiniune  34629  vonf1oonfo  35607  iota5f  36224  weiunse  37007  phpreu  38283  poimirlem25  38324  poimirlem26  38325  poimirlem28  38327  itgabsnc  38368  fsumshftd  39754  riotasv2s  39760  cdlemefs32sn1aw  41216  mzpsubmpt  43502  mzpsubst  43507  eq0rabdioph  43535  eqrabdioph  43536  rabdiophlem2  43557  fphpd  43571  monotuz  43696  monotoddzz  43698  oddcomabszz  43699  flcidc  43925  binomcxplemdvbinom  45091  binomcxplemdvsum  45093  binomcxplemnotnn0  45094  modelaxreplem3  45717  rfcnnnub  45784  disjinfi  45938  supxrleubrnmptf  46193  caucvgbf  46231  cvgcaule  46233  fsummulc1f  46315  fsumnncl  46316  fsumf1of  46318  fsumreclf  46320  fsumlessf  46321  fsumsermpt  46323  fmul01  46324  fmuldfeqlem1  46326  fmuldfeq  46327  fmul01lt1lem1  46328  fmul01lt1lem2  46329  fprodexp  46338  fprodabs2  46339  fprodcnlem  46343  climmulf  46348  climsuse  46352  climrecf  46353  climaddf  46359  0ellimcdiv  46391  climsubmpt  46402  climfveqf  46422  climinf2mpt  46456  climinfmpt  46457  fprodcncf  46642  dvmptmulf  46679  dvmptfprod  46687  iblspltprt  46715  stoweidlem3  46745  stoweidlem19  46761  stoweidlem22  46764  stoweidlem42  46784  fourierdlem31  46880  fourierdlem86  46934  fourierdlem89  46937  fourierdlem91  46939  fourierdlem112  46960  sge0f1o  47124  sge0lempt  47152  sge0iunmpt  47160  sge0ltfirpmpt2  47168  sge0isummpt2  47174  sge0xaddlem2  47176  sge0xadd  47177  vonhoire  47414  salpreimagelt  47449  smflim  47519  smfresal  47530  smfinflem  47559  eu2ndop1stv  47890