Theorem nfel1 2922

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

Syntax hints:  Ⅎwnf 1783   ∈ wcel 2108  Ⅎwnfc 2890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-nf 1784  df-cleq 2729  df-clel 2816  df-nfc 2892

This theorem is referenced by:  vtocl2gf  3572  vtocl3gf  3573  vtoclgaf  3576  vtocl2gaf  3579  vtocl2gafOLD  3580  vtocl3gaf  3581  vtocl3gafOLD  3582  nfop  4889  reusv2lem4  5401  reusv2  5403  rabxfrd  5417  pofun  5610  nfse  5659  fvmptf  7037  fmptcof  7150  fliftfuns  7334  riota2f  7412  ovmpos  7581  ov2gf  7582  elovmporab  7679  elovmporab1w  7680  elovmporab1  7681  ofmpteq  7720  fmpox  8092  offval22  8113  fvmpocurryd  8296  qliftfuns  8844  xpf1o  9179  iunfi  9383  wdom2d  9620  scottex  9925  dfac8clem  10072  ac6num  10519  pwfseqlem4a  10701  pwfseqlem4  10702  gruiin  10850  rlimcld2  15614  summolem3  15750  summolem2a  15751  zsum  15754  fsum  15756  sumss2  15762  fsumcvg2  15763  fsumclf  15774  fsumsplitf  15778  fsum2dlem  15806  fsumcom2  15810  fsumshftm  15817  fsum0diag2  15819  fsum00  15834  fsumabs  15837  fsumrlim  15847  fsumo1  15848  o1fsum  15849  fsumiun  15857  prodmolem3  15969  prodmolem2a  15970  zprod  15973  fprod  15977  prodss  15983  fprodser  15985  fprodm1s  16006  fprodp1s  16007  fprodabs  16010  fprodn0  16015  fprod2dlem  16016  fprodcom2  16020  fproddivf  16023  fprodsplitf  16024  fprodsplit1f  16026  fprodefsum  16131  pcmpt  16930  pcmptdvds  16932  gsumsnf  19971  gsumply1eq  22313  mdetralt2  22615  mdetunilem2  22619  fiuncmp  23412  elptr2  23582  ptcld  23621  ptcnplem  23629  ptcnp  23630  elmptrab  23835  utopsnneiplem  24256  prdsdsf  24377  prdsxmet  24379  fsumcn  24894  ovolfiniun  25536  ovoliunlem3  25539  ovoliun  25540  ovoliun2  25541  finiunmbl  25579  volfiniun  25582  iunmbl  25588  voliun  25589  itgfsum  25862  itgabs  25870  dvmptfsum  26013  dvfsumle  26060  dvfsumleOLD  26061  dvfsumabs  26063  dvfsumlem1  26066  dvfsumlem3  26069  dvfsumlem4  26070  dvfsumrlim  26072  dvfsumrlim2  26073  dvfsum2  26075  itgsubst  26090  fsumdvdscom  27228  fsumvma  27257  dchrisumlema  27532  dchrisumlem2  27534  dchrisumlem3  27535  fsumiunle  32831  locfinreflem  33839  esumcl  34031  esum0  34050  esumcst  34064  esumfsup  34071  esum2d  34094  measiun  34219  voliune  34230  volfiniune  34231  iota5f  35724  weiunse  36469  phpreu  37611  poimirlem25  37652  poimirlem26  37653  poimirlem28  37655  itgabsnc  37696  fsumshftd  38953  riotasv2s  38959  cdlemefs32sn1aw  40416  mzpsubmpt  42754  mzpsubst  42759  eq0rabdioph  42787  eqrabdioph  42788  rabdiophlem2  42813  fphpd  42827  monotuz  42953  monotoddzz  42955  oddcomabszz  42956  flcidc  43182  binomcxplemdvbinom  44372  binomcxplemdvsum  44374  binomcxplemnotnn0  44375  modelaxreplem3  44997  rfcnnnub  45041  disjinfi  45197  supxrleubrnmptf  45462  caucvgbf  45500  cvgcaule  45502  fsummulc1f  45586  fsumnncl  45587  fsumf1of  45589  fsumreclf  45591  fsumlessf  45592  fsumsermpt  45594  fmul01  45595  fmuldfeqlem1  45597  fmuldfeq  45598  fmul01lt1lem1  45599  fmul01lt1lem2  45600  fprodexp  45609  fprodabs2  45610  fprodcnlem  45614  climmulf  45619  climsuse  45623  climrecf  45624  climaddf  45630  0ellimcdiv  45664  climsubmpt  45675  climfveqf  45695  climinf2mpt  45729  climinfmpt  45730  fprodcncf  45915  dvmptmulf  45952  dvmptfprod  45960  iblspltprt  45988  stoweidlem3  46018  stoweidlem19  46034  stoweidlem22  46037  stoweidlem42  46057  fourierdlem31  46153  fourierdlem86  46207  fourierdlem89  46210  fourierdlem91  46212  fourierdlem112  46233  sge0f1o  46397  sge0lempt  46425  sge0iunmpt  46433  sge0ltfirpmpt2  46441  sge0isummpt2  46447  sge0xaddlem2  46449  sge0xadd  46450  vonhoire  46687  salpreimagelt  46722  smflim  46792  smfresal  46803  smfinflem  46832  eu2ndop1stv  47137