Theorem nfel1 2915

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

Syntax hints:  Ⅎwnf 1778   ∈ wcel 2099  Ⅎwnfc 2879

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-tru 1537  df-ex 1775  df-nf 1779  df-cleq 2720  df-clel 2806  df-nfc 2881

This theorem is referenced by:  vtocl2gf  3557  vtocl3gf  3558  vtoclgaf  3561  vtocl2gaf  3564  vtocl3gaf  3565  nfop  4886  reusv2lem4  5396  reusv2  5398  rabxfrd  5412  pofun  5603  nfse  5648  fvmptf  7021  fmptcof  7134  fliftfuns  7317  riota2f  7396  ovmpos  7564  ov2gf  7565  elovmporab  7662  elovmporab1w  7663  elovmporab1  7664  ofmpteq  7702  fmpox  8066  offval22  8088  fvmpocurryd  8271  qliftfuns  8817  xpf1o  9158  iunfi  9359  wdom2d  9598  scottex  9903  dfac8clem  10050  ac6num  10497  pwfseqlem4a  10679  pwfseqlem4  10680  gruiin  10828  rlimcld2  15549  summolem3  15687  summolem2a  15688  zsum  15691  fsum  15693  sumss2  15699  fsumcvg2  15700  fsumclf  15711  fsumsplitf  15715  fsum2dlem  15743  fsumcom2  15747  fsumshftm  15754  fsum0diag2  15756  fsum00  15771  fsumabs  15774  fsumrlim  15784  fsumo1  15785  o1fsum  15786  fsumiun  15794  prodmolem3  15904  prodmolem2a  15905  zprod  15908  fprod  15912  prodss  15918  fprodser  15920  fprodm1s  15941  fprodp1s  15942  fprodabs  15945  fprodn0  15950  fprod2dlem  15951  fprodcom2  15955  fproddivf  15958  fprodsplitf  15959  fprodsplit1f  15961  fprodefsum  16066  pcmpt  16855  pcmptdvds  16857  gsumsnf  19902  gsumply1eq  22222  mdetralt2  22505  mdetunilem2  22509  fiuncmp  23302  elptr2  23472  ptcld  23511  ptcnplem  23519  ptcnp  23520  elmptrab  23725  utopsnneiplem  24146  prdsdsf  24267  prdsxmet  24269  fsumcn  24782  ovolfiniun  25424  ovoliunlem3  25427  ovoliun  25428  ovoliun2  25429  finiunmbl  25467  volfiniun  25470  iunmbl  25476  voliun  25477  itgfsum  25750  itgabs  25758  dvmptfsum  25901  dvfsumle  25948  dvfsumleOLD  25949  dvfsumabs  25951  dvfsumlem1  25954  dvfsumlem3  25957  dvfsumlem4  25958  dvfsumrlim  25960  dvfsumrlim2  25961  dvfsum2  25963  itgsubst  25978  fsumdvdscom  27111  fsumvma  27140  dchrisumlema  27415  dchrisumlem2  27417  dchrisumlem3  27418  fsumiunle  32587  locfinreflem  33436  esumcl  33644  esum0  33663  esumcst  33677  esumfsup  33684  esum2d  33707  measiun  33832  voliune  33843  volfiniune  33844  iota5f  35313  phpreu  37072  poimirlem25  37113  poimirlem26  37114  poimirlem28  37116  itgabsnc  37157  fsumshftd  38419  riotasv2s  38425  cdlemefs32sn1aw  39882  mzpsubmpt  42154  mzpsubst  42159  eq0rabdioph  42187  eqrabdioph  42188  rabdiophlem2  42213  fphpd  42227  monotuz  42353  monotoddzz  42355  oddcomabszz  42356  flcidc  42589  binomcxplemdvbinom  43781  binomcxplemdvsum  43783  binomcxplemnotnn0  43784  rfcnnnub  44389  disjinfi  44556  supxrleubrnmptf  44824  caucvgbf  44863  cvgcaule  44865  fsummulc1f  44950  fsumnncl  44951  fsumf1of  44953  fsumreclf  44955  fsumlessf  44956  fsumsermpt  44958  fmul01  44959  fmuldfeqlem1  44961  fmuldfeq  44962  fmul01lt1lem1  44963  fmul01lt1lem2  44964  fprodexp  44973  fprodabs2  44974  fprodcnlem  44978  climmulf  44983  climsuse  44987  climrecf  44988  climaddf  44994  0ellimcdiv  45028  climsubmpt  45039  climfveqf  45059  climinf2mpt  45093  climinfmpt  45094  fprodcncf  45279  dvmptmulf  45316  iblspltprt  45352  stoweidlem3  45382  stoweidlem19  45398  stoweidlem22  45401  stoweidlem42  45421  fourierdlem31  45517  fourierdlem86  45571  fourierdlem89  45574  fourierdlem91  45576  fourierdlem112  45597  sge0f1o  45761  sge0lempt  45789  sge0iunmpt  45797  sge0ltfirpmpt2  45805  sge0isummpt2  45811  sge0xaddlem2  45813  sge0xadd  45814  vonhoire  46051  salpreimagelt  46086  smflim  46156  smfresal  46167  smfinflem  46196  eu2ndop1stv  46496