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  3516  vtocl3gf  3517  vtoclgaf  3520  vtocl2gaf  3523  vtocl2gafOLD  3524  vtocl3gaf  3525  vtocl3gafOLD  3526  nfop  4833  reusv2lem4  5339  reusv2  5341  rabxfrd  5355  pofun  5551  nfse  5599  fvmptf  6964  fmptcof  7078  fliftfuns  7263  riota2f  7342  ovmpos  7509  ov2gf  7510  elovmporab  7607  elovmporab1w  7608  elovmporab1  7609  ofmpteq  7648  fmpox  8014  offval22  8032  fvmpocurryd  8215  qliftfuns  8745  xpf1o  9071  iunfi  9247  wdom2d  9489  scottex  9803  dfac8clem  9948  ac6num  10395  pwfseqlem4a  10578  pwfseqlem4  10579  gruiin  10727  rlimcld2  15534  summolem3  15670  summolem2a  15671  zsum  15674  fsum  15676  sumss2  15682  fsumcvg2  15683  fsumclf  15694  fsumsplitf  15698  fsum2dlem  15726  fsumcom2  15730  fsumshftm  15737  fsum0diag2  15739  fsum00  15755  fsumabs  15758  fsumrlim  15768  fsumo1  15769  o1fsum  15770  fsumiun  15778  prodmolem3  15892  prodmolem2a  15893  zprod  15896  fprod  15900  prodss  15906  fprodser  15908  fprodm1s  15929  fprodp1s  15930  fprodabs  15933  fprodn0  15938  fprod2dlem  15939  fprodcom2  15943  fproddivf  15946  fprodsplitf  15947  fprodsplit1f  15949  fprodefsum  16054  pcmpt  16857  pcmptdvds  16859  gsumsnf  19922  gsumply1eq  22287  mdetralt2  22587  mdetunilem2  22591  fiuncmp  23382  elptr2  23552  ptcld  23591  ptcnplem  23599  ptcnp  23600  elmptrab  23805  utopsnneiplem  24225  prdsdsf  24345  prdsxmet  24347  fsumcn  24850  ovolfiniun  25481  ovoliunlem3  25484  ovoliun  25485  ovoliun2  25486  finiunmbl  25524  volfiniun  25527  iunmbl  25533  voliun  25534  itgfsum  25807  itgabs  25815  dvmptfsum  25955  dvfsumle  26001  dvfsumabs  26003  dvfsumlem1  26006  dvfsumlem3  26008  dvfsumlem4  26009  dvfsumrlim  26011  dvfsumrlim2  26012  dvfsum2  26014  itgsubst  26029  fsumdvdscom  27165  fsumvma  27193  dchrisumlema  27468  dchrisumlem2  27470  dchrisumlem3  27471  fsumiunle  32920  locfinreflem  34003  esumcl  34193  esum0  34212  esumcst  34226  esumfsup  34233  esum2d  34256  measiun  34381  voliune  34392  volfiniune  34393  iota5f  35925  weiunse  36669  phpreu  37942  poimirlem25  37983  poimirlem26  37984  poimirlem28  37986  itgabsnc  38027  fsumshftd  39415  riotasv2s  39421  cdlemefs32sn1aw  40877  mzpsubmpt  43192  mzpsubst  43197  eq0rabdioph  43225  eqrabdioph  43226  rabdiophlem2  43251  fphpd  43265  monotuz  43390  monotoddzz  43392  oddcomabszz  43393  flcidc  43619  binomcxplemdvbinom  44801  binomcxplemdvsum  44803  binomcxplemnotnn0  44804  modelaxreplem3  45428  rfcnnnub  45488  disjinfi  45643  supxrleubrnmptf  45900  caucvgbf  45938  cvgcaule  45940  fsummulc1f  46022  fsumnncl  46023  fsumf1of  46025  fsumreclf  46027  fsumlessf  46028  fsumsermpt  46030  fmul01  46031  fmuldfeqlem1  46033  fmuldfeq  46034  fmul01lt1lem1  46035  fmul01lt1lem2  46036  fprodexp  46045  fprodabs2  46046  fprodcnlem  46050  climmulf  46055  climsuse  46059  climrecf  46060  climaddf  46066  0ellimcdiv  46098  climsubmpt  46109  climfveqf  46129  climinf2mpt  46163  climinfmpt  46164  fprodcncf  46349  dvmptmulf  46386  dvmptfprod  46394  iblspltprt  46422  stoweidlem3  46452  stoweidlem19  46468  stoweidlem22  46471  stoweidlem42  46491  fourierdlem31  46587  fourierdlem86  46641  fourierdlem89  46644  fourierdlem91  46646  fourierdlem112  46667  sge0f1o  46831  sge0lempt  46859  sge0iunmpt  46867  sge0ltfirpmpt2  46875  sge0isummpt2  46881  sge0xaddlem2  46883  sge0xadd  46884  vonhoire  47121  salpreimagelt  47156  smflim  47226  smfresal  47237  smfinflem  47266  eu2ndop1stv  47588