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

Syntax hints:  Ⅎwnf 1785   ∈ wcel 2106  Ⅎwnfc 2883

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-nf 1786  df-cleq 2724  df-clel 2810  df-nfc 2885

This theorem is referenced by:  vtocl2gf  3560  vtocl3gf  3561  vtoclgaf  3564  vtocl2gaf  3567  vtocl3gaf  3568  nfop  4888  reusv2lem4  5398  reusv2  5400  rabxfrd  5414  pofun  5605  nfse  5650  fvmptf  7016  fmptcof  7124  fliftfuns  7307  riota2f  7386  ovmpos  7552  ov2gf  7553  elovmporab  7648  elovmporab1w  7649  elovmporab1  7650  ofmpteq  7688  fmpox  8049  offval22  8070  fvmpocurryd  8252  qliftfuns  8794  xpf1o  9135  iunfi  9336  wdom2d  9571  scottex  9876  dfac8clem  10023  ac6num  10470  pwfseqlem4a  10652  pwfseqlem4  10653  gruiin  10801  rlimcld2  15518  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  15873  prodmolem2a  15874  zprod  15877  fprod  15881  prodss  15887  fprodser  15889  fprodm1s  15910  fprodp1s  15911  fprodabs  15914  fprodn0  15919  fprod2dlem  15920  fprodcom2  15924  fproddivf  15927  fprodsplitf  15928  fprodsplit1f  15930  fprodefsum  16034  pcmpt  16821  pcmptdvds  16823  gsumsnf  19815  gsumply1eq  21820  mdetralt2  22102  mdetunilem2  22106  fiuncmp  22899  elptr2  23069  ptcld  23108  ptcnplem  23116  ptcnp  23117  elmptrab  23322  utopsnneiplem  23743  prdsdsf  23864  prdsxmet  23866  fsumcn  24377  ovolfiniun  25009  ovoliunlem3  25012  ovoliun  25013  ovoliun2  25014  finiunmbl  25052  volfiniun  25055  iunmbl  25061  voliun  25062  itgfsum  25335  itgabs  25343  dvmptfsum  25483  dvfsumle  25529  dvfsumabs  25531  dvfsumlem1  25534  dvfsumlem3  25536  dvfsumlem4  25537  dvfsumrlim  25539  dvfsumrlim2  25540  dvfsum2  25542  itgsubst  25557  fsumdvdscom  26678  fsumvma  26705  dchrisumlema  26980  dchrisumlem2  26982  dchrisumlem3  26983  fsumiunle  32022  locfinreflem  32808  esumcl  33016  esum0  33035  esumcst  33049  esumfsup  33056  esum2d  33079  measiun  33204  voliune  33215  volfiniune  33216  iota5f  34681  gg-dvfsumle  35170  phpreu  36460  poimirlem25  36501  poimirlem26  36502  poimirlem28  36504  itgabsnc  36545  fsumshftd  37810  riotasv2s  37816  cdlemefs32sn1aw  39273  mzpsubmpt  41466  mzpsubst  41471  eq0rabdioph  41499  eqrabdioph  41500  rabdiophlem2  41525  fphpd  41539  monotuz  41665  monotoddzz  41667  oddcomabszz  41668  flcidc  41901  binomcxplemdvbinom  43097  binomcxplemdvsum  43099  binomcxplemnotnn0  43100  rfcnnnub  43705  disjinfi  43876  supxrleubrnmptf  44147  caucvgbf  44186  cvgcaule  44188  fsummulc1f  44273  fsumnncl  44274  fsumf1of  44276  fsumreclf  44278  fsumlessf  44279  fsumsermpt  44281  fmul01  44282  fmuldfeqlem1  44284  fmuldfeq  44285  fmul01lt1lem1  44286  fmul01lt1lem2  44287  fprodexp  44296  fprodabs2  44297  fprodcnlem  44301  climmulf  44306  climsuse  44310  climrecf  44311  climaddf  44317  0ellimcdiv  44351  climsubmpt  44362  climfveqf  44382  climinf2mpt  44416  climinfmpt  44417  fprodcncf  44602  dvmptmulf  44639  iblspltprt  44675  stoweidlem3  44705  stoweidlem19  44721  stoweidlem22  44724  stoweidlem42  44744  fourierdlem31  44840  fourierdlem86  44894  fourierdlem89  44897  fourierdlem91  44899  fourierdlem112  44920  sge0f1o  45084  sge0lempt  45112  sge0iunmpt  45120  sge0ltfirpmpt2  45128  sge0isummpt2  45134  sge0xaddlem2  45136  sge0xadd  45137  vonhoire  45374  salpreimagelt  45409  smflim  45479  smfresal  45490  smfinflem  45519  eu2ndop1stv  45819