Theorem nfel1 2996

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

Syntax hints:  Ⅎwnf 1784   ∈ wcel 2114  Ⅎwnfc 2963

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-cleq 2816  df-clel 2895  df-nfc 2965

This theorem is referenced by:  vtocl2gf  3572  vtocl3gf  3573  vtoclgaf  3575  vtocl2gaf  3578  vtocl3gaf  3579  nfop  4821  reusv2lem4  5304  reusv2  5306  rabxfrd  5320  pofun  5493  nfse  5532  fvmptf  6791  fmptcof  6894  fliftfuns  7069  riota2f  7140  ovmpos  7300  ov2gf  7301  elovmporab  7393  elovmporab1w  7394  elovmporab1  7395  ofmpteq  7430  fmpox  7767  offval22  7785  fvmpocurryd  7939  qliftfuns  8386  xpf1o  8681  iunfi  8814  wdom2d  9046  scottex  9316  dfac8clem  9460  ac6num  9903  pwfseqlem4a  10085  pwfseqlem4  10086  gruiin  10234  rlimcld2  14937  summolem3  15073  summolem2a  15074  zsum  15077  fsum  15079  sumss2  15085  fsumcvg2  15086  fsumsplitf  15100  fsum2dlem  15127  fsumcom2  15131  fsumshftm  15138  fsum0diag2  15140  fsum00  15155  fsumabs  15158  fsumrlim  15168  fsumo1  15169  o1fsum  15170  fsumiun  15178  prodmolem3  15289  prodmolem2a  15290  zprod  15293  fprod  15297  prodss  15303  fprodser  15305  fprodm1s  15326  fprodp1s  15327  fprodabs  15330  fprodn0  15335  fprod2dlem  15336  fprodcom2  15340  fproddivf  15343  fprodsplitf  15344  fprodsplit1f  15346  fprodefsum  15450  pcmpt  16230  pcmptdvds  16232  gsumsnf  19075  gsumply1eq  20475  mdetralt2  21220  mdetunilem2  21224  fiuncmp  22014  elptr2  22184  ptcld  22223  ptcnplem  22231  ptcnp  22232  elmptrab  22437  utopsnneiplem  22858  prdsdsf  22979  prdsxmet  22981  fsumcn  23480  ovolfiniun  24104  ovoliunlem3  24107  ovoliun  24108  ovoliun2  24109  finiunmbl  24147  volfiniun  24150  iunmbl  24156  voliun  24157  itgfsum  24429  itgabs  24437  dvmptfsum  24574  dvfsumle  24620  dvfsumabs  24622  dvfsumlem1  24625  dvfsumlem3  24627  dvfsumlem4  24628  dvfsumrlim  24630  dvfsumrlim2  24631  dvfsum2  24633  itgsubst  24648  fsumdvdscom  25764  fsumvma  25791  dchrisumlema  26066  dchrisumlem2  26068  dchrisumlem3  26069  fsumiunle  30547  locfinreflem  31106  esumcl  31291  esum0  31310  esumcst  31324  esumfsup  31331  esum2d  31354  measiun  31479  voliune  31490  volfiniune  31491  iota5f  32957  phpreu  34878  poimirlem25  34919  poimirlem26  34920  poimirlem28  34922  itgabsnc  34963  fsumshftd  36090  riotasv2s  36096  cdlemefs32sn1aw  37552  mzpsubmpt  39347  mzpsubst  39352  eq0rabdioph  39380  eqrabdioph  39381  rabdiophlem2  39406  fphpd  39420  monotuz  39545  monotoddzz  39547  oddcomabszz  39548  flcidc  39781  binomcxplemdvbinom  40692  binomcxplemdvsum  40694  binomcxplemnotnn0  40695  rfcnnnub  41300  supxrleubrnmptf  41734  fsumclf  41857  fsummulc1f  41858  fsumnncl  41859  fsumf1of  41862  fsumreclf  41864  fsumlessf  41865  fsumsermpt  41867  fmul01  41868  fmuldfeqlem1  41870  fmuldfeq  41871  fmul01lt1lem1  41872  fmul01lt1lem2  41873  fprodexp  41882  fprodabs2  41883  fprodcnlem  41887  climmulf  41892  climsuse  41896  climrecf  41897  climaddf  41903  0ellimcdiv  41937  climsubmpt  41948  climfveqf  41968  climinf2mpt  42002  climinfmpt  42003  fprodcncf  42191  dvmptmulf  42229  iblspltprt  42265  stoweidlem3  42295  stoweidlem19  42311  stoweidlem22  42314  stoweidlem42  42334  fourierdlem31  42430  fourierdlem86  42484  fourierdlem89  42487  fourierdlem91  42489  fourierdlem112  42510  sge0f1o  42671  sge0lempt  42699  sge0iunmpt  42707  sge0ltfirpmpt2  42715  sge0isummpt2  42721  sge0xaddlem2  42723  sge0xadd  42724  vonhoire  42961  salpreimagelt  42993  smflim  43060  smfresal  43070  smfinflem  43098  eu2ndop1stv  43331