Theorem nfel1 2919

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

Syntax hints:  Ⅎwnf 1779   ∈ wcel 2105  Ⅎwnfc 2887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1539  df-ex 1776  df-nf 1780  df-cleq 2726  df-clel 2813  df-nfc 2889

This theorem is referenced by:  vtocl2gf  3571  vtocl3gf  3572  vtoclgaf  3575  vtocl2gaf  3578  vtocl2gafOLD  3579  vtocl3gaf  3580  vtocl3gafOLD  3581  nfop  4893  reusv2lem4  5406  reusv2  5408  rabxfrd  5422  pofun  5614  nfse  5662  fvmptf  7036  fmptcof  7149  fliftfuns  7333  riota2f  7411  ovmpos  7580  ov2gf  7581  elovmporab  7678  elovmporab1w  7679  elovmporab1  7680  ofmpteq  7719  fmpox  8090  offval22  8111  fvmpocurryd  8294  qliftfuns  8842  xpf1o  9177  iunfi  9380  wdom2d  9617  scottex  9922  dfac8clem  10069  ac6num  10516  pwfseqlem4a  10698  pwfseqlem4  10699  gruiin  10847  rlimcld2  15610  summolem3  15746  summolem2a  15747  zsum  15750  fsum  15752  sumss2  15758  fsumcvg2  15759  fsumclf  15770  fsumsplitf  15774  fsum2dlem  15802  fsumcom2  15806  fsumshftm  15813  fsum0diag2  15815  fsum00  15830  fsumabs  15833  fsumrlim  15843  fsumo1  15844  o1fsum  15845  fsumiun  15853  prodmolem3  15965  prodmolem2a  15966  zprod  15969  fprod  15973  prodss  15979  fprodser  15981  fprodm1s  16002  fprodp1s  16003  fprodabs  16006  fprodn0  16011  fprod2dlem  16012  fprodcom2  16016  fproddivf  16019  fprodsplitf  16020  fprodsplit1f  16022  fprodefsum  16127  pcmpt  16925  pcmptdvds  16927  gsumsnf  19985  gsumply1eq  22328  mdetralt2  22630  mdetunilem2  22634  fiuncmp  23427  elptr2  23597  ptcld  23636  ptcnplem  23644  ptcnp  23645  elmptrab  23850  utopsnneiplem  24271  prdsdsf  24392  prdsxmet  24394  fsumcn  24907  ovolfiniun  25549  ovoliunlem3  25552  ovoliun  25553  ovoliun2  25554  finiunmbl  25592  volfiniun  25595  iunmbl  25601  voliun  25602  itgfsum  25876  itgabs  25884  dvmptfsum  26027  dvfsumle  26074  dvfsumleOLD  26075  dvfsumabs  26077  dvfsumlem1  26080  dvfsumlem3  26083  dvfsumlem4  26084  dvfsumrlim  26086  dvfsumrlim2  26087  dvfsum2  26089  itgsubst  26104  fsumdvdscom  27242  fsumvma  27271  dchrisumlema  27546  dchrisumlem2  27548  dchrisumlem3  27549  fsumiunle  32835  locfinreflem  33800  esumcl  34010  esum0  34029  esumcst  34043  esumfsup  34050  esum2d  34073  measiun  34198  voliune  34209  volfiniune  34210  iota5f  35703  weiunse  36450  phpreu  37590  poimirlem25  37631  poimirlem26  37632  poimirlem28  37634  itgabsnc  37675  fsumshftd  38933  riotasv2s  38939  cdlemefs32sn1aw  40396  mzpsubmpt  42730  mzpsubst  42735  eq0rabdioph  42763  eqrabdioph  42764  rabdiophlem2  42789  fphpd  42803  monotuz  42929  monotoddzz  42931  oddcomabszz  42932  flcidc  43158  binomcxplemdvbinom  44348  binomcxplemdvsum  44350  binomcxplemnotnn0  44351  modelaxreplem3  44944  rfcnnnub  44973  disjinfi  45134  supxrleubrnmptf  45400  caucvgbf  45439  cvgcaule  45441  fsummulc1f  45526  fsumnncl  45527  fsumf1of  45529  fsumreclf  45531  fsumlessf  45532  fsumsermpt  45534  fmul01  45535  fmuldfeqlem1  45537  fmuldfeq  45538  fmul01lt1lem1  45539  fmul01lt1lem2  45540  fprodexp  45549  fprodabs2  45550  fprodcnlem  45554  climmulf  45559  climsuse  45563  climrecf  45564  climaddf  45570  0ellimcdiv  45604  climsubmpt  45615  climfveqf  45635  climinf2mpt  45669  climinfmpt  45670  fprodcncf  45855  dvmptmulf  45892  dvmptfprod  45900  iblspltprt  45928  stoweidlem3  45958  stoweidlem19  45974  stoweidlem22  45977  stoweidlem42  45997  fourierdlem31  46093  fourierdlem86  46147  fourierdlem89  46150  fourierdlem91  46152  fourierdlem112  46173  sge0f1o  46337  sge0lempt  46365  sge0iunmpt  46373  sge0ltfirpmpt2  46381  sge0isummpt2  46387  sge0xaddlem2  46389  sge0xadd  46390  vonhoire  46627  salpreimagelt  46662  smflim  46732  smfresal  46743  smfinflem  46772  eu2ndop1stv  47074