Theorem nfel1 2938

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

This proof depends on syntax axioms:  Ⅎwnf 1815   ∈ wcel 2144  Ⅎwnfc 2907

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-nf 1816  df-cleq 2752  df-clel 2835  df-nfc 2909

This theorem is used by:  vtocl2gf  3531  vtocl3gf  3532  vtoclgaf  3535  vtocl2gaf  3538  vtocl3gaf  3539  nfop  4848  reusv2lem4  5362  reusv2  5364  rabxfrd  5378  pofun  5576  nfse  5624  fvmptf  7015  fmptcof  7131  fliftfuns  7322  riota2f  7401  ovmpos  7568  ov2gf  7569  elovmporab  7667  elovmporab1w  7668  elovmporab1  7669  ofmpteq  7716  fmpox  8078  offval22  8099  fvmpocurryd  8288  qliftfuns  8825  xpf1o  9158  iunfi  9332  wdom2d  9574  scottexOLD  9934  dfac8clem  10111  ac6num  10557  pwfseqlem4a  10746  pwfseqlem4  10747  gruiin  10895  rlimcld2  15745  summolem3  15880  summolem2a  15881  zsum  15884  fsum  15886  sumss2  15892  fsumcvg2  15893  fsumclf  15904  fsumsplitf  15908  fsum2dlem  15936  fsumcom2  15940  fsumshftm  15947  fsum0diag2  15949  fsum00  15965  fsumabs  15968  fsumrlim  15978  fsumo1  15979  o1fsum  15980  fsumiun  15988  prodmolem3  16100  prodmolem2a  16101  zprod  16104  fprod  16108  prodss  16114  fprodser  16116  fprodm1s  16137  fprodp1s  16138  fprodabs  16141  fprodn0  16146  fprod2dlem  16147  fprodcom2  16151  fproddivf  16154  fprodsplitf  16155  fprodsplit1f  16157  fprodefsum  16261  pcmpt  17070  pcmptdvds  17072  gsumsnf  20167  gsumply1eq  22627  mdetralt2  22924  mdetunilem2  22928  fiuncmp  23722  elptr2  23893  ptcld  23932  ptcnplem  23940  ptcnp  23941  elmptrab  24146  utopsnneiplem  24566  prdsdsf  24686  prdsxmet  24688  fsumcn  25191  ovolfiniun  25822  ovoliunlem3  25825  ovoliun  25826  ovoliun2  25827  finiunmbl  25865  volfiniun  25868  iunmbl  25874  voliun  25875  itgfsum  26147  itgabs  26155  dvmptfsum  26295  dvfsumle  26341  dvfsumabs  26343  dvfsumlem1  26346  dvfsumlem3  26348  dvfsumlem4  26349  dvfsumrlim  26351  dvfsumrlim2  26352  dvfsum2  26354  itgsubst  26369  fsumdvdscom  27512  fsumvma  27540  dchrisumlema  27815  dchrisumlem2  27817  dchrisumlem3  27818  fsumiunle  33462  locfinreflem  34514  esumcl  34704  esum0  34723  esumcst  34737  esumfsup  34744  esum2d  34767  measiun  34893  voliune  34904  volfiniune  34905  vonf1oonfo  35940  iota5f  36531  weiunse  37298  phpreu  38570  poimirlem25  38606  poimirlem26  38607  poimirlem28  38609  itgabsnc  38650  fsumshftd  40052  riotasv2s  40058  cdlemefs32sn1aw  41514  mzpsubmpt  43796  mzpsubst  43801  eq0rabdioph  43829  eqrabdioph  43830  rabdiophlem2  43851  fphpd  43865  monotuz  43990  monotoddzz  43992  oddcomabszz  43993  flcidc  44214  binomcxplemdvbinom  45379  binomcxplemdvsum  45381  binomcxplemnotnn0  45382  modelaxreplem3  46012  rfcnnnub  46095  disjinfi  46249  supxrleubrnmptf  46503  caucvgbf  46541  cvgcaule  46543  fsummulc1f  46625  fsumnncl  46626  fsumf1of  46628  fsumreclf  46630  fsumlessf  46631  fsumsermpt  46633  fmul01  46634  fmuldfeqlem1  46636  fmuldfeq  46637  fmul01lt1lem1  46638  fmul01lt1lem2  46639  fprodexp  46648  fprodabs2  46649  fprodcnlem  46653  climmulf  46658  climsuse  46662  climrecf  46663  climaddf  46669  0ellimcdiv  46701  climsubmpt  46712  climfveqf  46732  climinf2mpt  46766  climinfmpt  46767  fprodcncf  46952  dvmptmulf  46989  dvmptfprod  46997  iblspltprt  47025  stoweidlem3  47055  stoweidlem19  47071  stoweidlem22  47074  stoweidlem42  47094  fourierdlem31  47190  fourierdlem86  47244  fourierdlem89  47247  fourierdlem91  47249  fourierdlem112  47270  sge0f1o  47434  sge0lempt  47462  sge0iunmpt  47470  sge0ltfirpmpt2  47478  sge0isummpt2  47484  sge0xaddlem2  47486  sge0xadd  47487  vonhoire  47724  salpreimagelt  47759  smflim  47829  smfresal  47840  smfinflem  47869  eu2ndop1stv  48237