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  3535  vtocl3gf  3536  vtoclgaf  3539  vtocl2gaf  3542  vtocl2gafOLD  3543  vtocl3gaf  3544  vtocl3gafOLD  3545  nfop  4849  reusv2lem4  5351  reusv2  5353  rabxfrd  5367  pofun  5557  nfse  5605  fvmptf  6971  fmptcof  7084  fliftfuns  7271  riota2f  7350  ovmpos  7517  ov2gf  7518  elovmporab  7615  elovmporab1w  7616  elovmporab1  7617  ofmpteq  7656  fmpox  8025  offval22  8044  fvmpocurryd  8227  qliftfuns  8754  xpf1o  9080  iunfi  9270  wdom2d  9509  scottex  9814  dfac8clem  9961  ac6num  10408  pwfseqlem4a  10590  pwfseqlem4  10591  gruiin  10739  rlimcld2  15520  summolem3  15656  summolem2a  15657  zsum  15660  fsum  15662  sumss2  15668  fsumcvg2  15669  fsumclf  15680  fsumsplitf  15684  fsum2dlem  15712  fsumcom2  15716  fsumshftm  15723  fsum0diag2  15725  fsum00  15740  fsumabs  15743  fsumrlim  15753  fsumo1  15754  o1fsum  15755  fsumiun  15763  prodmolem3  15875  prodmolem2a  15876  zprod  15879  fprod  15883  prodss  15889  fprodser  15891  fprodm1s  15912  fprodp1s  15913  fprodabs  15916  fprodn0  15921  fprod2dlem  15922  fprodcom2  15926  fproddivf  15929  fprodsplitf  15930  fprodsplit1f  15932  fprodefsum  16037  pcmpt  16839  pcmptdvds  16841  gsumsnf  19867  gsumply1eq  22229  mdetralt2  22529  mdetunilem2  22533  fiuncmp  23324  elptr2  23494  ptcld  23533  ptcnplem  23541  ptcnp  23542  elmptrab  23747  utopsnneiplem  24168  prdsdsf  24288  prdsxmet  24290  fsumcn  24794  ovolfiniun  25435  ovoliunlem3  25438  ovoliun  25439  ovoliun2  25440  finiunmbl  25478  volfiniun  25481  iunmbl  25487  voliun  25488  itgfsum  25761  itgabs  25769  dvmptfsum  25912  dvfsumle  25959  dvfsumleOLD  25960  dvfsumabs  25962  dvfsumlem1  25965  dvfsumlem3  25968  dvfsumlem4  25969  dvfsumrlim  25971  dvfsumrlim2  25972  dvfsum2  25974  itgsubst  25989  fsumdvdscom  27128  fsumvma  27157  dchrisumlema  27432  dchrisumlem2  27434  dchrisumlem3  27435  fsumiunle  32804  locfinreflem  33823  esumcl  34013  esum0  34032  esumcst  34046  esumfsup  34053  esum2d  34076  measiun  34201  voliune  34212  volfiniune  34213  iota5f  35704  weiunse  36449  phpreu  37591  poimirlem25  37632  poimirlem26  37633  poimirlem28  37635  itgabsnc  37676  fsumshftd  38938  riotasv2s  38944  cdlemefs32sn1aw  40401  mzpsubmpt  42724  mzpsubst  42729  eq0rabdioph  42757  eqrabdioph  42758  rabdiophlem2  42783  fphpd  42797  monotuz  42923  monotoddzz  42925  oddcomabszz  42926  flcidc  43152  binomcxplemdvbinom  44335  binomcxplemdvsum  44337  binomcxplemnotnn0  44338  modelaxreplem3  44963  rfcnnnub  45023  disjinfi  45179  supxrleubrnmptf  45440  caucvgbf  45478  cvgcaule  45480  fsummulc1f  45562  fsumnncl  45563  fsumf1of  45565  fsumreclf  45567  fsumlessf  45568  fsumsermpt  45570  fmul01  45571  fmuldfeqlem1  45573  fmuldfeq  45574  fmul01lt1lem1  45575  fmul01lt1lem2  45576  fprodexp  45585  fprodabs2  45586  fprodcnlem  45590  climmulf  45595  climsuse  45599  climrecf  45600  climaddf  45606  0ellimcdiv  45640  climsubmpt  45651  climfveqf  45671  climinf2mpt  45705  climinfmpt  45706  fprodcncf  45891  dvmptmulf  45928  dvmptfprod  45936  iblspltprt  45964  stoweidlem3  45994  stoweidlem19  46010  stoweidlem22  46013  stoweidlem42  46033  fourierdlem31  46129  fourierdlem86  46183  fourierdlem89  46186  fourierdlem91  46188  fourierdlem112  46209  sge0f1o  46373  sge0lempt  46401  sge0iunmpt  46409  sge0ltfirpmpt2  46417  sge0isummpt2  46423  sge0xaddlem2  46425  sge0xadd  46426  vonhoire  46663  salpreimagelt  46698  smflim  46768  smfresal  46779  smfinflem  46808  eu2ndop1stv  47119