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  19859  gsumply1eq  22172  mdetralt2  22472  mdetunilem2  22476  fiuncmp  23267  elptr2  23437  ptcld  23476  ptcnplem  23484  ptcnp  23485  elmptrab  23690  utopsnneiplem  24111  prdsdsf  24231  prdsxmet  24233  fsumcn  24737  ovolfiniun  25378  ovoliunlem3  25381  ovoliun  25382  ovoliun2  25383  finiunmbl  25421  volfiniun  25424  iunmbl  25430  voliun  25431  itgfsum  25704  itgabs  25712  dvmptfsum  25855  dvfsumle  25902  dvfsumleOLD  25903  dvfsumabs  25905  dvfsumlem1  25908  dvfsumlem3  25911  dvfsumlem4  25912  dvfsumrlim  25914  dvfsumrlim2  25915  dvfsum2  25917  itgsubst  25932  fsumdvdscom  27071  fsumvma  27100  dchrisumlema  27375  dchrisumlem2  27377  dchrisumlem3  27378  fsumiunle  32727  locfinreflem  33803  esumcl  33993  esum0  34012  esumcst  34026  esumfsup  34033  esum2d  34056  measiun  34181  voliune  34192  volfiniune  34193  iota5f  35684  weiunse  36429  phpreu  37571  poimirlem25  37612  poimirlem26  37613  poimirlem28  37615  itgabsnc  37656  fsumshftd  38918  riotasv2s  38924  cdlemefs32sn1aw  40381  mzpsubmpt  42704  mzpsubst  42709  eq0rabdioph  42737  eqrabdioph  42738  rabdiophlem2  42763  fphpd  42777  monotuz  42903  monotoddzz  42905  oddcomabszz  42906  flcidc  43132  binomcxplemdvbinom  44315  binomcxplemdvsum  44317  binomcxplemnotnn0  44318  modelaxreplem3  44943  rfcnnnub  45003  disjinfi  45159  supxrleubrnmptf  45420  caucvgbf  45458  cvgcaule  45460  fsummulc1f  45542  fsumnncl  45543  fsumf1of  45545  fsumreclf  45547  fsumlessf  45548  fsumsermpt  45550  fmul01  45551  fmuldfeqlem1  45553  fmuldfeq  45554  fmul01lt1lem1  45555  fmul01lt1lem2  45556  fprodexp  45565  fprodabs2  45566  fprodcnlem  45570  climmulf  45575  climsuse  45579  climrecf  45580  climaddf  45586  0ellimcdiv  45620  climsubmpt  45631  climfveqf  45651  climinf2mpt  45685  climinfmpt  45686  fprodcncf  45871  dvmptmulf  45908  dvmptfprod  45916  iblspltprt  45944  stoweidlem3  45974  stoweidlem19  45990  stoweidlem22  45993  stoweidlem42  46013  fourierdlem31  46109  fourierdlem86  46163  fourierdlem89  46166  fourierdlem91  46168  fourierdlem112  46189  sge0f1o  46353  sge0lempt  46381  sge0iunmpt  46389  sge0ltfirpmpt2  46397  sge0isummpt2  46403  sge0xaddlem2  46405  sge0xadd  46406  vonhoire  46643  salpreimagelt  46678  smflim  46748  smfresal  46759  smfinflem  46788  eu2ndop1stv  47099