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

Syntax hints:  Ⅎwnf 1785   ∈ wcel 2114  Ⅎwnfc 2883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-nf 1786  df-cleq 2728  df-clel 2811  df-nfc 2885

This theorem is referenced by:  vtocl2gf  3515  vtocl3gf  3516  vtoclgaf  3519  vtocl2gaf  3522  vtocl2gafOLD  3523  vtocl3gaf  3524  vtocl3gafOLD  3525  nfop  4832  reusv2lem4  5343  reusv2  5345  rabxfrd  5359  pofun  5557  nfse  5605  fvmptf  6969  fmptcof  7083  fliftfuns  7269  riota2f  7348  ovmpos  7515  ov2gf  7516  elovmporab  7613  elovmporab1w  7614  elovmporab1  7615  ofmpteq  7654  fmpox  8020  offval22  8038  fvmpocurryd  8221  qliftfuns  8751  xpf1o  9077  iunfi  9253  wdom2d  9495  scottex  9809  dfac8clem  9954  ac6num  10401  pwfseqlem4a  10584  pwfseqlem4  10585  gruiin  10733  rlimcld2  15540  summolem3  15676  summolem2a  15677  zsum  15680  fsum  15682  sumss2  15688  fsumcvg2  15689  fsumclf  15700  fsumsplitf  15704  fsum2dlem  15732  fsumcom2  15736  fsumshftm  15743  fsum0diag2  15745  fsum00  15761  fsumabs  15764  fsumrlim  15774  fsumo1  15775  o1fsum  15776  fsumiun  15784  prodmolem3  15898  prodmolem2a  15899  zprod  15902  fprod  15906  prodss  15912  fprodser  15914  fprodm1s  15935  fprodp1s  15936  fprodabs  15939  fprodn0  15944  fprod2dlem  15945  fprodcom2  15949  fproddivf  15952  fprodsplitf  15953  fprodsplit1f  15955  fprodefsum  16060  pcmpt  16863  pcmptdvds  16865  gsumsnf  19928  gsumply1eq  22274  mdetralt2  22574  mdetunilem2  22578  fiuncmp  23369  elptr2  23539  ptcld  23578  ptcnplem  23586  ptcnp  23587  elmptrab  23792  utopsnneiplem  24212  prdsdsf  24332  prdsxmet  24334  fsumcn  24837  ovolfiniun  25468  ovoliunlem3  25471  ovoliun  25472  ovoliun2  25473  finiunmbl  25511  volfiniun  25514  iunmbl  25520  voliun  25521  itgfsum  25794  itgabs  25802  dvmptfsum  25942  dvfsumle  25988  dvfsumabs  25990  dvfsumlem1  25993  dvfsumlem3  25995  dvfsumlem4  25996  dvfsumrlim  25998  dvfsumrlim2  25999  dvfsum2  26001  itgsubst  26016  fsumdvdscom  27148  fsumvma  27176  dchrisumlema  27451  dchrisumlem2  27453  dchrisumlem3  27454  fsumiunle  32902  locfinreflem  33984  esumcl  34174  esum0  34193  esumcst  34207  esumfsup  34214  esum2d  34237  measiun  34362  voliune  34373  volfiniune  34374  iota5f  35906  weiunse  36650  phpreu  37925  poimirlem25  37966  poimirlem26  37967  poimirlem28  37969  itgabsnc  38010  fsumshftd  39398  riotasv2s  39404  cdlemefs32sn1aw  40860  mzpsubmpt  43175  mzpsubst  43180  eq0rabdioph  43208  eqrabdioph  43209  rabdiophlem2  43230  fphpd  43244  monotuz  43369  monotoddzz  43371  oddcomabszz  43372  flcidc  43598  binomcxplemdvbinom  44780  binomcxplemdvsum  44782  binomcxplemnotnn0  44783  modelaxreplem3  45407  rfcnnnub  45467  disjinfi  45622  supxrleubrnmptf  45879  caucvgbf  45917  cvgcaule  45919  fsummulc1f  46001  fsumnncl  46002  fsumf1of  46004  fsumreclf  46006  fsumlessf  46007  fsumsermpt  46009  fmul01  46010  fmuldfeqlem1  46012  fmuldfeq  46013  fmul01lt1lem1  46014  fmul01lt1lem2  46015  fprodexp  46024  fprodabs2  46025  fprodcnlem  46029  climmulf  46034  climsuse  46038  climrecf  46039  climaddf  46045  0ellimcdiv  46077  climsubmpt  46088  climfveqf  46108  climinf2mpt  46142  climinfmpt  46143  fprodcncf  46328  dvmptmulf  46365  dvmptfprod  46373  iblspltprt  46401  stoweidlem3  46431  stoweidlem19  46447  stoweidlem22  46450  stoweidlem42  46470  fourierdlem31  46566  fourierdlem86  46620  fourierdlem89  46623  fourierdlem91  46625  fourierdlem112  46646  sge0f1o  46810  sge0lempt  46838  sge0iunmpt  46846  sge0ltfirpmpt2  46854  sge0isummpt2  46860  sge0xaddlem2  46862  sge0xadd  46863  vonhoire  47100  salpreimagelt  47135  smflim  47205  smfresal  47216  smfinflem  47245  eu2ndop1stv  47573