Theorem nfel1 2925

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

Syntax hints:  Ⅎwnf 1790   ∈ wcel 2110  Ⅎwnfc 2889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1545  df-ex 1787  df-nf 1791  df-cleq 2732  df-clel 2818  df-nfc 2891

This theorem is referenced by:  vtocl2gf  3507  vtocl3gf  3508  vtoclgaf  3511  vtocl2gaf  3514  vtocl3gaf  3515  nfop  4826  reusv2lem4  5328  reusv2  5330  rabxfrd  5344  pofun  5522  nfse  5565  fvmptf  6893  fmptcof  6999  fliftfuns  7182  riota2f  7254  ovmpos  7416  ov2gf  7417  elovmporab  7510  elovmporab1w  7511  elovmporab1  7512  ofmpteq  7550  fmpox  7901  offval22  7920  fvmpocurryd  8079  qliftfuns  8585  xpf1o  8917  iunfi  9095  wdom2d  9327  scottex  9654  dfac8clem  9799  ac6num  10246  pwfseqlem4a  10428  pwfseqlem4  10429  gruiin  10577  rlimcld2  15298  summolem3  15437  summolem2a  15438  zsum  15441  fsum  15443  sumss2  15449  fsumcvg2  15450  fsumclf  15461  fsumsplitf  15465  fsum2dlem  15493  fsumcom2  15497  fsumshftm  15504  fsum0diag2  15506  fsum00  15521  fsumabs  15524  fsumrlim  15534  fsumo1  15535  o1fsum  15536  fsumiun  15544  prodmolem3  15654  prodmolem2a  15655  zprod  15658  fprod  15662  prodss  15668  fprodser  15670  fprodm1s  15691  fprodp1s  15692  fprodabs  15695  fprodn0  15700  fprod2dlem  15701  fprodcom2  15705  fproddivf  15708  fprodsplitf  15709  fprodsplit1f  15711  fprodefsum  15815  pcmpt  16604  pcmptdvds  16606  gsumsnf  19565  gsumply1eq  21487  mdetralt2  21769  mdetunilem2  21773  fiuncmp  22566  elptr2  22736  ptcld  22775  ptcnplem  22783  ptcnp  22784  elmptrab  22989  utopsnneiplem  23410  prdsdsf  23531  prdsxmet  23533  fsumcn  24044  ovolfiniun  24676  ovoliunlem3  24679  ovoliun  24680  ovoliun2  24681  finiunmbl  24719  volfiniun  24722  iunmbl  24728  voliun  24729  itgfsum  25002  itgabs  25010  dvmptfsum  25150  dvfsumle  25196  dvfsumabs  25198  dvfsumlem1  25201  dvfsumlem3  25203  dvfsumlem4  25204  dvfsumrlim  25206  dvfsumrlim2  25207  dvfsum2  25209  itgsubst  25224  fsumdvdscom  26345  fsumvma  26372  dchrisumlema  26647  dchrisumlem2  26649  dchrisumlem3  26650  fsumiunle  31152  locfinreflem  31799  esumcl  32007  esum0  32026  esumcst  32040  esumfsup  32047  esum2d  32070  measiun  32195  voliune  32206  volfiniune  32207  iota5f  33678  phpreu  35770  poimirlem25  35811  poimirlem26  35812  poimirlem28  35814  itgabsnc  35855  fsumshftd  36975  riotasv2s  36981  cdlemefs32sn1aw  38437  mzpsubmpt  40574  mzpsubst  40579  eq0rabdioph  40607  eqrabdioph  40608  rabdiophlem2  40633  fphpd  40647  monotuz  40772  monotoddzz  40774  oddcomabszz  40775  flcidc  41008  binomcxplemdvbinom  41953  binomcxplemdvsum  41955  binomcxplemnotnn0  41956  rfcnnnub  42561  disjinfi  42713  supxrleubrnmptf  42973  fsummulc1f  43094  fsumnncl  43095  fsumf1of  43097  fsumreclf  43099  fsumlessf  43100  fsumsermpt  43102  fmul01  43103  fmuldfeqlem1  43105  fmuldfeq  43106  fmul01lt1lem1  43107  fmul01lt1lem2  43108  fprodexp  43117  fprodabs2  43118  fprodcnlem  43122  climmulf  43127  climsuse  43131  climrecf  43132  climaddf  43138  0ellimcdiv  43172  climsubmpt  43183  climfveqf  43203  climinf2mpt  43237  climinfmpt  43238  fprodcncf  43423  dvmptmulf  43460  iblspltprt  43496  stoweidlem3  43526  stoweidlem19  43542  stoweidlem22  43545  stoweidlem42  43565  fourierdlem31  43661  fourierdlem86  43715  fourierdlem89  43718  fourierdlem91  43720  fourierdlem112  43741  sge0f1o  43902  sge0lempt  43930  sge0iunmpt  43938  sge0ltfirpmpt2  43946  sge0isummpt2  43952  sge0xaddlem2  43954  sge0xadd  43955  vonhoire  44192  salpreimagelt  44224  smflim  44291  smfresal  44301  smfinflem  44329  eu2ndop1stv  44596