Theorem nfel1 2994

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

Syntax hints:  Ⅎwnf 1780   ∈ wcel 2110  Ⅎwnfc 2961

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-cleq 2814  df-clel 2893  df-nfc 2963

This theorem is referenced by:  vtocl2gf  3569  vtocl3gf  3570  vtoclgaf  3572  vtocl2gaf  3575  vtocl3gaf  3576  nfop  4812  reusv2lem4  5293  reusv2  5295  rabxfrd  5309  pofun  5485  nfse  5524  fvmptf  6783  fmptcof  6886  fliftfuns  7061  riota2f  7132  ovmpos  7292  ov2gf  7293  elovmporab  7385  elovmporab1w  7386  elovmporab1  7387  ofmpteq  7422  fmpox  7759  offval22  7777  fvmpocurryd  7931  qliftfuns  8378  xpf1o  8673  iunfi  8806  wdom2d  9038  scottex  9308  dfac8clem  9452  ac6num  9895  pwfseqlem4a  10077  pwfseqlem4  10078  gruiin  10226  rlimcld2  14929  summolem3  15065  summolem2a  15066  zsum  15069  fsum  15071  sumss2  15077  fsumcvg2  15078  fsumsplitf  15092  fsum2dlem  15119  fsumcom2  15123  fsumshftm  15130  fsum0diag2  15132  fsum00  15147  fsumabs  15150  fsumrlim  15160  fsumo1  15161  o1fsum  15162  fsumiun  15170  prodmolem3  15281  prodmolem2a  15282  zprod  15285  fprod  15289  prodss  15295  fprodser  15297  fprodm1s  15318  fprodp1s  15319  fprodabs  15322  fprodn0  15327  fprod2dlem  15328  fprodcom2  15332  fproddivf  15335  fprodsplitf  15336  fprodsplit1f  15338  fprodefsum  15442  pcmpt  16222  pcmptdvds  16224  gsumsnf  19067  gsumply1eq  20467  mdetralt2  21212  mdetunilem2  21216  fiuncmp  22006  elptr2  22176  ptcld  22215  ptcnplem  22223  ptcnp  22224  elmptrab  22429  utopsnneiplem  22850  prdsdsf  22971  prdsxmet  22973  fsumcn  23472  ovolfiniun  24096  ovoliunlem3  24099  ovoliun  24100  ovoliun2  24101  finiunmbl  24139  volfiniun  24142  iunmbl  24148  voliun  24149  itgfsum  24421  itgabs  24429  dvmptfsum  24566  dvfsumle  24612  dvfsumabs  24614  dvfsumlem1  24617  dvfsumlem3  24619  dvfsumlem4  24620  dvfsumrlim  24622  dvfsumrlim2  24623  dvfsum2  24625  itgsubst  24640  fsumdvdscom  25756  fsumvma  25783  dchrisumlema  26058  dchrisumlem2  26060  dchrisumlem3  26061  fsumiunle  30540  locfinreflem  31099  esumcl  31284  esum0  31303  esumcst  31317  esumfsup  31324  esum2d  31347  measiun  31472  voliune  31483  volfiniune  31484  iota5f  32950  phpreu  34870  poimirlem25  34911  poimirlem26  34912  poimirlem28  34914  itgabsnc  34955  fsumshftd  36082  riotasv2s  36088  cdlemefs32sn1aw  37544  mzpsubmpt  39333  mzpsubst  39338  eq0rabdioph  39366  eqrabdioph  39367  rabdiophlem2  39392  fphpd  39406  monotuz  39531  monotoddzz  39533  oddcomabszz  39534  flcidc  39767  binomcxplemdvbinom  40678  binomcxplemdvsum  40680  binomcxplemnotnn0  40681  rfcnnnub  41286  supxrleubrnmptf  41720  fsumclf  41843  fsummulc1f  41844  fsumnncl  41845  fsumf1of  41848  fsumreclf  41850  fsumlessf  41851  fsumsermpt  41853  fmul01  41854  fmuldfeqlem1  41856  fmuldfeq  41857  fmul01lt1lem1  41858  fmul01lt1lem2  41859  fprodexp  41868  fprodabs2  41869  fprodcnlem  41873  climmulf  41878  climsuse  41882  climrecf  41883  climaddf  41889  0ellimcdiv  41923  climsubmpt  41934  climfveqf  41954  climinf2mpt  41988  climinfmpt  41989  fprodcncf  42177  dvmptmulf  42215  iblspltprt  42251  stoweidlem3  42282  stoweidlem19  42298  stoweidlem22  42301  stoweidlem42  42321  fourierdlem31  42417  fourierdlem86  42471  fourierdlem89  42474  fourierdlem91  42476  fourierdlem112  42497  sge0f1o  42658  sge0lempt  42686  sge0iunmpt  42694  sge0ltfirpmpt2  42702  sge0isummpt2  42708  sge0xaddlem2  42710  sge0xadd  42711  vonhoire  42948  salpreimagelt  42980  smflim  43047  smfresal  43057  smfinflem  43085  eu2ndop1stv  43318