Theorem nfel1 2908

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

Syntax hints:  Ⅎwnf 1783   ∈ wcel 2109  Ⅎwnfc 2876

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-nf 1784  df-cleq 2721  df-clel 2803  df-nfc 2878

This theorem is referenced by:  vtocl2gf  3527  vtocl3gf  3528  vtoclgaf  3531  vtocl2gaf  3534  vtocl2gafOLD  3535  vtocl3gaf  3536  vtocl3gafOLD  3537  nfop  4840  reusv2lem4  5340  reusv2  5342  rabxfrd  5356  pofun  5545  nfse  5593  fvmptf  6951  fmptcof  7064  fliftfuns  7251  riota2f  7330  ovmpos  7497  ov2gf  7498  elovmporab  7595  elovmporab1w  7596  elovmporab1  7597  ofmpteq  7636  fmpox  8002  offval22  8021  fvmpocurryd  8204  qliftfuns  8731  xpf1o  9056  iunfi  9233  wdom2d  9472  scottex  9781  dfac8clem  9926  ac6num  10373  pwfseqlem4a  10555  pwfseqlem4  10556  gruiin  10704  rlimcld2  15485  summolem3  15621  summolem2a  15622  zsum  15625  fsum  15627  sumss2  15633  fsumcvg2  15634  fsumclf  15645  fsumsplitf  15649  fsum2dlem  15677  fsumcom2  15681  fsumshftm  15688  fsum0diag2  15690  fsum00  15705  fsumabs  15708  fsumrlim  15718  fsumo1  15719  o1fsum  15720  fsumiun  15728  prodmolem3  15840  prodmolem2a  15841  zprod  15844  fprod  15848  prodss  15854  fprodser  15856  fprodm1s  15877  fprodp1s  15878  fprodabs  15881  fprodn0  15886  fprod2dlem  15887  fprodcom2  15891  fproddivf  15894  fprodsplitf  15895  fprodsplit1f  15897  fprodefsum  16002  pcmpt  16804  pcmptdvds  16806  gsumsnf  19832  gsumply1eq  22194  mdetralt2  22494  mdetunilem2  22498  fiuncmp  23289  elptr2  23459  ptcld  23498  ptcnplem  23506  ptcnp  23507  elmptrab  23712  utopsnneiplem  24133  prdsdsf  24253  prdsxmet  24255  fsumcn  24759  ovolfiniun  25400  ovoliunlem3  25403  ovoliun  25404  ovoliun2  25405  finiunmbl  25443  volfiniun  25446  iunmbl  25452  voliun  25453  itgfsum  25726  itgabs  25734  dvmptfsum  25877  dvfsumle  25924  dvfsumleOLD  25925  dvfsumabs  25927  dvfsumlem1  25930  dvfsumlem3  25933  dvfsumlem4  25934  dvfsumrlim  25936  dvfsumrlim2  25937  dvfsum2  25939  itgsubst  25954  fsumdvdscom  27093  fsumvma  27122  dchrisumlema  27397  dchrisumlem2  27399  dchrisumlem3  27400  fsumiunle  32774  locfinreflem  33807  esumcl  33997  esum0  34016  esumcst  34030  esumfsup  34037  esum2d  34060  measiun  34185  voliune  34196  volfiniune  34197  iota5f  35697  weiunse  36442  phpreu  37584  poimirlem25  37625  poimirlem26  37626  poimirlem28  37628  itgabsnc  37669  fsumshftd  38931  riotasv2s  38937  cdlemefs32sn1aw  40393  mzpsubmpt  42716  mzpsubst  42721  eq0rabdioph  42749  eqrabdioph  42750  rabdiophlem2  42775  fphpd  42789  monotuz  42914  monotoddzz  42916  oddcomabszz  42917  flcidc  43143  binomcxplemdvbinom  44326  binomcxplemdvsum  44328  binomcxplemnotnn0  44329  modelaxreplem3  44954  rfcnnnub  45014  disjinfi  45170  supxrleubrnmptf  45430  caucvgbf  45468  cvgcaule  45470  fsummulc1f  45552  fsumnncl  45553  fsumf1of  45555  fsumreclf  45557  fsumlessf  45558  fsumsermpt  45560  fmul01  45561  fmuldfeqlem1  45563  fmuldfeq  45564  fmul01lt1lem1  45565  fmul01lt1lem2  45566  fprodexp  45575  fprodabs2  45576  fprodcnlem  45580  climmulf  45585  climsuse  45589  climrecf  45590  climaddf  45596  0ellimcdiv  45630  climsubmpt  45641  climfveqf  45661  climinf2mpt  45695  climinfmpt  45696  fprodcncf  45881  dvmptmulf  45918  dvmptfprod  45926  iblspltprt  45954  stoweidlem3  45984  stoweidlem19  46000  stoweidlem22  46003  stoweidlem42  46023  fourierdlem31  46119  fourierdlem86  46173  fourierdlem89  46176  fourierdlem91  46178  fourierdlem112  46199  sge0f1o  46363  sge0lempt  46391  sge0iunmpt  46399  sge0ltfirpmpt2  46407  sge0isummpt2  46413  sge0xaddlem2  46415  sge0xadd  46416  vonhoire  46653  salpreimagelt  46688  smflim  46758  smfresal  46769  smfinflem  46798  eu2ndop1stv  47109