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  3538  vtocl3gf  3539  vtoclgaf  3542  vtocl2gaf  3545  vtocl2gafOLD  3546  vtocl3gaf  3547  vtocl3gafOLD  3548  nfop  4853  reusv2lem4  5356  reusv2  5358  rabxfrd  5372  pofun  5564  nfse  5612  fvmptf  6989  fmptcof  7102  fliftfuns  7289  riota2f  7368  ovmpos  7537  ov2gf  7538  elovmporab  7635  elovmporab1w  7636  elovmporab1  7637  ofmpteq  7676  fmpox  8046  offval22  8067  fvmpocurryd  8250  qliftfuns  8777  xpf1o  9103  iunfi  9294  wdom2d  9533  scottex  9838  dfac8clem  9985  ac6num  10432  pwfseqlem4a  10614  pwfseqlem4  10615  gruiin  10763  rlimcld2  15544  summolem3  15680  summolem2a  15681  zsum  15684  fsum  15686  sumss2  15692  fsumcvg2  15693  fsumclf  15704  fsumsplitf  15708  fsum2dlem  15736  fsumcom2  15740  fsumshftm  15747  fsum0diag2  15749  fsum00  15764  fsumabs  15767  fsumrlim  15777  fsumo1  15778  o1fsum  15779  fsumiun  15787  prodmolem3  15899  prodmolem2a  15900  zprod  15903  fprod  15907  prodss  15913  fprodser  15915  fprodm1s  15936  fprodp1s  15937  fprodabs  15940  fprodn0  15945  fprod2dlem  15946  fprodcom2  15950  fproddivf  15953  fprodsplitf  15954  fprodsplit1f  15956  fprodefsum  16061  pcmpt  16863  pcmptdvds  16865  gsumsnf  19883  gsumply1eq  22196  mdetralt2  22496  mdetunilem2  22500  fiuncmp  23291  elptr2  23461  ptcld  23500  ptcnplem  23508  ptcnp  23509  elmptrab  23714  utopsnneiplem  24135  prdsdsf  24255  prdsxmet  24257  fsumcn  24761  ovolfiniun  25402  ovoliunlem3  25405  ovoliun  25406  ovoliun2  25407  finiunmbl  25445  volfiniun  25448  iunmbl  25454  voliun  25455  itgfsum  25728  itgabs  25736  dvmptfsum  25879  dvfsumle  25926  dvfsumleOLD  25927  dvfsumabs  25929  dvfsumlem1  25932  dvfsumlem3  25935  dvfsumlem4  25936  dvfsumrlim  25938  dvfsumrlim2  25939  dvfsum2  25941  itgsubst  25956  fsumdvdscom  27095  fsumvma  27124  dchrisumlema  27399  dchrisumlem2  27401  dchrisumlem3  27402  fsumiunle  32754  locfinreflem  33830  esumcl  34020  esum0  34039  esumcst  34053  esumfsup  34060  esum2d  34083  measiun  34208  voliune  34219  volfiniune  34220  iota5f  35711  weiunse  36456  phpreu  37598  poimirlem25  37639  poimirlem26  37640  poimirlem28  37642  itgabsnc  37683  fsumshftd  38945  riotasv2s  38951  cdlemefs32sn1aw  40408  mzpsubmpt  42731  mzpsubst  42736  eq0rabdioph  42764  eqrabdioph  42765  rabdiophlem2  42790  fphpd  42804  monotuz  42930  monotoddzz  42932  oddcomabszz  42933  flcidc  43159  binomcxplemdvbinom  44342  binomcxplemdvsum  44344  binomcxplemnotnn0  44345  modelaxreplem3  44970  rfcnnnub  45030  disjinfi  45186  supxrleubrnmptf  45447  caucvgbf  45485  cvgcaule  45487  fsummulc1f  45569  fsumnncl  45570  fsumf1of  45572  fsumreclf  45574  fsumlessf  45575  fsumsermpt  45577  fmul01  45578  fmuldfeqlem1  45580  fmuldfeq  45581  fmul01lt1lem1  45582  fmul01lt1lem2  45583  fprodexp  45592  fprodabs2  45593  fprodcnlem  45597  climmulf  45602  climsuse  45606  climrecf  45607  climaddf  45613  0ellimcdiv  45647  climsubmpt  45658  climfveqf  45678  climinf2mpt  45712  climinfmpt  45713  fprodcncf  45898  dvmptmulf  45935  dvmptfprod  45943  iblspltprt  45971  stoweidlem3  46001  stoweidlem19  46017  stoweidlem22  46020  stoweidlem42  46040  fourierdlem31  46136  fourierdlem86  46190  fourierdlem89  46193  fourierdlem91  46195  fourierdlem112  46216  sge0f1o  46380  sge0lempt  46408  sge0iunmpt  46416  sge0ltfirpmpt2  46424  sge0isummpt2  46430  sge0xaddlem2  46432  sge0xadd  46433  vonhoire  46670  salpreimagelt  46705  smflim  46775  smfresal  46786  smfinflem  46815  eu2ndop1stv  47126