Theorem nfel1 2920

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

Syntax hints:  Ⅎwnf 1786   ∈ wcel 2107  Ⅎwnfc 2884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-nf 1787  df-cleq 2725  df-clel 2811  df-nfc 2886

This theorem is referenced by:  vtocl2gf  3561  vtocl3gf  3562  vtoclgaf  3565  vtocl2gaf  3568  vtocl3gaf  3569  nfop  4890  reusv2lem4  5400  reusv2  5402  rabxfrd  5416  pofun  5607  nfse  5652  fvmptf  7020  fmptcof  7128  fliftfuns  7311  riota2f  7390  ovmpos  7556  ov2gf  7557  elovmporab  7652  elovmporab1w  7653  elovmporab1  7654  ofmpteq  7692  fmpox  8053  offval22  8074  fvmpocurryd  8256  qliftfuns  8798  xpf1o  9139  iunfi  9340  wdom2d  9575  scottex  9880  dfac8clem  10027  ac6num  10474  pwfseqlem4a  10656  pwfseqlem4  10657  gruiin  10805  rlimcld2  15522  summolem3  15660  summolem2a  15661  zsum  15664  fsum  15666  sumss2  15672  fsumcvg2  15673  fsumclf  15684  fsumsplitf  15688  fsum2dlem  15716  fsumcom2  15720  fsumshftm  15727  fsum0diag2  15729  fsum00  15744  fsumabs  15747  fsumrlim  15757  fsumo1  15758  o1fsum  15759  fsumiun  15767  prodmolem3  15877  prodmolem2a  15878  zprod  15881  fprod  15885  prodss  15891  fprodser  15893  fprodm1s  15914  fprodp1s  15915  fprodabs  15918  fprodn0  15923  fprod2dlem  15924  fprodcom2  15928  fproddivf  15931  fprodsplitf  15932  fprodsplit1f  15934  fprodefsum  16038  pcmpt  16825  pcmptdvds  16827  gsumsnf  19821  gsumply1eq  21829  mdetralt2  22111  mdetunilem2  22115  fiuncmp  22908  elptr2  23078  ptcld  23117  ptcnplem  23125  ptcnp  23126  elmptrab  23331  utopsnneiplem  23752  prdsdsf  23873  prdsxmet  23875  fsumcn  24386  ovolfiniun  25018  ovoliunlem3  25021  ovoliun  25022  ovoliun2  25023  finiunmbl  25061  volfiniun  25064  iunmbl  25070  voliun  25071  itgfsum  25344  itgabs  25352  dvmptfsum  25492  dvfsumle  25538  dvfsumabs  25540  dvfsumlem1  25543  dvfsumlem3  25545  dvfsumlem4  25546  dvfsumrlim  25548  dvfsumrlim2  25549  dvfsum2  25551  itgsubst  25566  fsumdvdscom  26689  fsumvma  26716  dchrisumlema  26991  dchrisumlem2  26993  dchrisumlem3  26994  fsumiunle  32035  locfinreflem  32820  esumcl  33028  esum0  33047  esumcst  33061  esumfsup  33068  esum2d  33091  measiun  33216  voliune  33227  volfiniune  33228  iota5f  34693  gg-dvfsumle  35182  phpreu  36472  poimirlem25  36513  poimirlem26  36514  poimirlem28  36516  itgabsnc  36557  fsumshftd  37822  riotasv2s  37828  cdlemefs32sn1aw  39285  mzpsubmpt  41481  mzpsubst  41486  eq0rabdioph  41514  eqrabdioph  41515  rabdiophlem2  41540  fphpd  41554  monotuz  41680  monotoddzz  41682  oddcomabszz  41683  flcidc  41916  binomcxplemdvbinom  43112  binomcxplemdvsum  43114  binomcxplemnotnn0  43115  rfcnnnub  43720  disjinfi  43891  supxrleubrnmptf  44161  caucvgbf  44200  cvgcaule  44202  fsummulc1f  44287  fsumnncl  44288  fsumf1of  44290  fsumreclf  44292  fsumlessf  44293  fsumsermpt  44295  fmul01  44296  fmuldfeqlem1  44298  fmuldfeq  44299  fmul01lt1lem1  44300  fmul01lt1lem2  44301  fprodexp  44310  fprodabs2  44311  fprodcnlem  44315  climmulf  44320  climsuse  44324  climrecf  44325  climaddf  44331  0ellimcdiv  44365  climsubmpt  44376  climfveqf  44396  climinf2mpt  44430  climinfmpt  44431  fprodcncf  44616  dvmptmulf  44653  iblspltprt  44689  stoweidlem3  44719  stoweidlem19  44735  stoweidlem22  44738  stoweidlem42  44758  fourierdlem31  44854  fourierdlem86  44908  fourierdlem89  44911  fourierdlem91  44913  fourierdlem112  44934  sge0f1o  45098  sge0lempt  45126  sge0iunmpt  45134  sge0ltfirpmpt2  45142  sge0isummpt2  45148  sge0xaddlem2  45150  sge0xadd  45151  vonhoire  45388  salpreimagelt  45423  smflim  45493  smfresal  45504  smfinflem  45533  eu2ndop1stv  45833