Theorem nfel1 2916

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

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

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 2709

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 2729  df-clel 2812  df-nfc 2886

This theorem is referenced by:  vtocl2gf  3529  vtocl3gf  3530  vtoclgaf  3533  vtocl2gaf  3536  vtocl2gafOLD  3537  vtocl3gaf  3538  vtocl3gafOLD  3539  nfop  4847  reusv2lem4  5348  reusv2  5350  rabxfrd  5364  pofun  5558  nfse  5606  fvmptf  6971  fmptcof  7085  fliftfuns  7270  riota2f  7349  ovmpos  7516  ov2gf  7517  elovmporab  7614  elovmporab1w  7615  elovmporab1  7616  ofmpteq  7655  fmpox  8021  offval22  8040  fvmpocurryd  8223  qliftfuns  8753  xpf1o  9079  iunfi  9255  wdom2d  9497  scottex  9809  dfac8clem  9954  ac6num  10401  pwfseqlem4a  10584  pwfseqlem4  10585  gruiin  10733  rlimcld2  15513  summolem3  15649  summolem2a  15650  zsum  15653  fsum  15655  sumss2  15661  fsumcvg2  15662  fsumclf  15673  fsumsplitf  15677  fsum2dlem  15705  fsumcom2  15709  fsumshftm  15716  fsum0diag2  15718  fsum00  15733  fsumabs  15736  fsumrlim  15746  fsumo1  15747  o1fsum  15748  fsumiun  15756  prodmolem3  15868  prodmolem2a  15869  zprod  15872  fprod  15876  prodss  15882  fprodser  15884  fprodm1s  15905  fprodp1s  15906  fprodabs  15909  fprodn0  15914  fprod2dlem  15915  fprodcom2  15919  fproddivf  15922  fprodsplitf  15923  fprodsplit1f  15925  fprodefsum  16030  pcmpt  16832  pcmptdvds  16834  gsumsnf  19894  gsumply1eq  22265  mdetralt2  22565  mdetunilem2  22569  fiuncmp  23360  elptr2  23530  ptcld  23569  ptcnplem  23577  ptcnp  23578  elmptrab  23783  utopsnneiplem  24203  prdsdsf  24323  prdsxmet  24325  fsumcn  24829  ovolfiniun  25470  ovoliunlem3  25473  ovoliun  25474  ovoliun2  25475  finiunmbl  25513  volfiniun  25516  iunmbl  25522  voliun  25523  itgfsum  25796  itgabs  25804  dvmptfsum  25947  dvfsumle  25994  dvfsumleOLD  25995  dvfsumabs  25997  dvfsumlem1  26000  dvfsumlem3  26003  dvfsumlem4  26004  dvfsumrlim  26006  dvfsumrlim2  26007  dvfsum2  26009  itgsubst  26024  fsumdvdscom  27163  fsumvma  27192  dchrisumlema  27467  dchrisumlem2  27469  dchrisumlem3  27470  fsumiunle  32921  locfinreflem  34018  esumcl  34208  esum0  34227  esumcst  34241  esumfsup  34248  esum2d  34271  measiun  34396  voliune  34407  volfiniune  34408  iota5f  35940  weiunse  36684  phpreu  37855  poimirlem25  37896  poimirlem26  37897  poimirlem28  37899  itgabsnc  37940  fsumshftd  39328  riotasv2s  39334  cdlemefs32sn1aw  40790  mzpsubmpt  43100  mzpsubst  43105  eq0rabdioph  43133  eqrabdioph  43134  rabdiophlem2  43159  fphpd  43173  monotuz  43298  monotoddzz  43300  oddcomabszz  43301  flcidc  43527  binomcxplemdvbinom  44709  binomcxplemdvsum  44711  binomcxplemnotnn0  44712  modelaxreplem3  45336  rfcnnnub  45396  disjinfi  45551  supxrleubrnmptf  45809  caucvgbf  45847  cvgcaule  45849  fsummulc1f  45931  fsumnncl  45932  fsumf1of  45934  fsumreclf  45936  fsumlessf  45937  fsumsermpt  45939  fmul01  45940  fmuldfeqlem1  45942  fmuldfeq  45943  fmul01lt1lem1  45944  fmul01lt1lem2  45945  fprodexp  45954  fprodabs2  45955  fprodcnlem  45959  climmulf  45964  climsuse  45968  climrecf  45969  climaddf  45975  0ellimcdiv  46007  climsubmpt  46018  climfveqf  46038  climinf2mpt  46072  climinfmpt  46073  fprodcncf  46258  dvmptmulf  46295  dvmptfprod  46303  iblspltprt  46331  stoweidlem3  46361  stoweidlem19  46377  stoweidlem22  46380  stoweidlem42  46400  fourierdlem31  46496  fourierdlem86  46550  fourierdlem89  46553  fourierdlem91  46555  fourierdlem112  46576  sge0f1o  46740  sge0lempt  46768  sge0iunmpt  46776  sge0ltfirpmpt2  46784  sge0isummpt2  46790  sge0xaddlem2  46792  sge0xadd  46793  vonhoire  47030  salpreimagelt  47065  smflim  47135  smfresal  47146  smfinflem  47175  eu2ndop1stv  47485