Theorem nfel1 2915

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

Syntax hints:  Ⅎwnf 1783   ∈ wcel 2108  Ⅎwnfc 2883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-nf 1784  df-cleq 2727  df-clel 2809  df-nfc 2885

This theorem is referenced by:  vtocl2gf  3551  vtocl3gf  3552  vtoclgaf  3555  vtocl2gaf  3558  vtocl2gafOLD  3559  vtocl3gaf  3560  vtocl3gafOLD  3561  nfop  4865  reusv2lem4  5371  reusv2  5373  rabxfrd  5387  pofun  5579  nfse  5628  fvmptf  7006  fmptcof  7119  fliftfuns  7306  riota2f  7384  ovmpos  7553  ov2gf  7554  elovmporab  7651  elovmporab1w  7652  elovmporab1  7653  ofmpteq  7692  fmpox  8064  offval22  8085  fvmpocurryd  8268  qliftfuns  8816  xpf1o  9151  iunfi  9353  wdom2d  9592  scottex  9897  dfac8clem  10044  ac6num  10491  pwfseqlem4a  10673  pwfseqlem4  10674  gruiin  10822  rlimcld2  15592  summolem3  15728  summolem2a  15729  zsum  15732  fsum  15734  sumss2  15740  fsumcvg2  15741  fsumclf  15752  fsumsplitf  15756  fsum2dlem  15784  fsumcom2  15788  fsumshftm  15795  fsum0diag2  15797  fsum00  15812  fsumabs  15815  fsumrlim  15825  fsumo1  15826  o1fsum  15827  fsumiun  15835  prodmolem3  15947  prodmolem2a  15948  zprod  15951  fprod  15955  prodss  15961  fprodser  15963  fprodm1s  15984  fprodp1s  15985  fprodabs  15988  fprodn0  15993  fprod2dlem  15994  fprodcom2  15998  fproddivf  16001  fprodsplitf  16002  fprodsplit1f  16004  fprodefsum  16109  pcmpt  16910  pcmptdvds  16912  gsumsnf  19932  gsumply1eq  22245  mdetralt2  22545  mdetunilem2  22549  fiuncmp  23340  elptr2  23510  ptcld  23549  ptcnplem  23557  ptcnp  23558  elmptrab  23763  utopsnneiplem  24184  prdsdsf  24304  prdsxmet  24306  fsumcn  24810  ovolfiniun  25452  ovoliunlem3  25455  ovoliun  25456  ovoliun2  25457  finiunmbl  25495  volfiniun  25498  iunmbl  25504  voliun  25505  itgfsum  25778  itgabs  25786  dvmptfsum  25929  dvfsumle  25976  dvfsumleOLD  25977  dvfsumabs  25979  dvfsumlem1  25982  dvfsumlem3  25985  dvfsumlem4  25986  dvfsumrlim  25988  dvfsumrlim2  25989  dvfsum2  25991  itgsubst  26006  fsumdvdscom  27145  fsumvma  27174  dchrisumlema  27449  dchrisumlem2  27451  dchrisumlem3  27452  fsumiunle  32754  locfinreflem  33817  esumcl  34007  esum0  34026  esumcst  34040  esumfsup  34047  esum2d  34070  measiun  34195  voliune  34206  volfiniune  34207  iota5f  35687  weiunse  36432  phpreu  37574  poimirlem25  37615  poimirlem26  37616  poimirlem28  37618  itgabsnc  37659  fsumshftd  38916  riotasv2s  38922  cdlemefs32sn1aw  40379  mzpsubmpt  42713  mzpsubst  42718  eq0rabdioph  42746  eqrabdioph  42747  rabdiophlem2  42772  fphpd  42786  monotuz  42912  monotoddzz  42914  oddcomabszz  42915  flcidc  43141  binomcxplemdvbinom  44325  binomcxplemdvsum  44327  binomcxplemnotnn0  44328  modelaxreplem3  44953  rfcnnnub  45008  disjinfi  45164  supxrleubrnmptf  45426  caucvgbf  45464  cvgcaule  45466  fsummulc1f  45548  fsumnncl  45549  fsumf1of  45551  fsumreclf  45553  fsumlessf  45554  fsumsermpt  45556  fmul01  45557  fmuldfeqlem1  45559  fmuldfeq  45560  fmul01lt1lem1  45561  fmul01lt1lem2  45562  fprodexp  45571  fprodabs2  45572  fprodcnlem  45576  climmulf  45581  climsuse  45585  climrecf  45586  climaddf  45592  0ellimcdiv  45626  climsubmpt  45637  climfveqf  45657  climinf2mpt  45691  climinfmpt  45692  fprodcncf  45877  dvmptmulf  45914  dvmptfprod  45922  iblspltprt  45950  stoweidlem3  45980  stoweidlem19  45996  stoweidlem22  45999  stoweidlem42  46019  fourierdlem31  46115  fourierdlem86  46169  fourierdlem89  46172  fourierdlem91  46174  fourierdlem112  46195  sge0f1o  46359  sge0lempt  46387  sge0iunmpt  46395  sge0ltfirpmpt2  46403  sge0isummpt2  46409  sge0xaddlem2  46411  sge0xadd  46412  vonhoire  46649  salpreimagelt  46684  smflim  46754  smfresal  46765  smfinflem  46794  eu2ndop1stv  47102