Theorem nfel1 2909

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

Syntax hints:  Ⅎwnf 1783   ∈ wcel 2109  Ⅎwnfc 2877

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702

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 2722  df-clel 2804  df-nfc 2879

This theorem is referenced by:  vtocl2gf  3541  vtocl3gf  3542  vtoclgaf  3545  vtocl2gaf  3548  vtocl2gafOLD  3549  vtocl3gaf  3550  vtocl3gafOLD  3551  nfop  4856  reusv2lem4  5359  reusv2  5361  rabxfrd  5375  pofun  5567  nfse  5615  fvmptf  6992  fmptcof  7105  fliftfuns  7292  riota2f  7371  ovmpos  7540  ov2gf  7541  elovmporab  7638  elovmporab1w  7639  elovmporab1  7640  ofmpteq  7679  fmpox  8049  offval22  8070  fvmpocurryd  8253  qliftfuns  8780  xpf1o  9109  iunfi  9301  wdom2d  9540  scottex  9845  dfac8clem  9992  ac6num  10439  pwfseqlem4a  10621  pwfseqlem4  10622  gruiin  10770  rlimcld2  15551  summolem3  15687  summolem2a  15688  zsum  15691  fsum  15693  sumss2  15699  fsumcvg2  15700  fsumclf  15711  fsumsplitf  15715  fsum2dlem  15743  fsumcom2  15747  fsumshftm  15754  fsum0diag2  15756  fsum00  15771  fsumabs  15774  fsumrlim  15784  fsumo1  15785  o1fsum  15786  fsumiun  15794  prodmolem3  15906  prodmolem2a  15907  zprod  15910  fprod  15914  prodss  15920  fprodser  15922  fprodm1s  15943  fprodp1s  15944  fprodabs  15947  fprodn0  15952  fprod2dlem  15953  fprodcom2  15957  fproddivf  15960  fprodsplitf  15961  fprodsplit1f  15963  fprodefsum  16068  pcmpt  16870  pcmptdvds  16872  gsumsnf  19890  gsumply1eq  22203  mdetralt2  22503  mdetunilem2  22507  fiuncmp  23298  elptr2  23468  ptcld  23507  ptcnplem  23515  ptcnp  23516  elmptrab  23721  utopsnneiplem  24142  prdsdsf  24262  prdsxmet  24264  fsumcn  24768  ovolfiniun  25409  ovoliunlem3  25412  ovoliun  25413  ovoliun2  25414  finiunmbl  25452  volfiniun  25455  iunmbl  25461  voliun  25462  itgfsum  25735  itgabs  25743  dvmptfsum  25886  dvfsumle  25933  dvfsumleOLD  25934  dvfsumabs  25936  dvfsumlem1  25939  dvfsumlem3  25942  dvfsumlem4  25943  dvfsumrlim  25945  dvfsumrlim2  25946  dvfsum2  25948  itgsubst  25963  fsumdvdscom  27102  fsumvma  27131  dchrisumlema  27406  dchrisumlem2  27408  dchrisumlem3  27409  fsumiunle  32761  locfinreflem  33837  esumcl  34027  esum0  34046  esumcst  34060  esumfsup  34067  esum2d  34090  measiun  34215  voliune  34226  volfiniune  34227  iota5f  35718  weiunse  36463  phpreu  37605  poimirlem25  37646  poimirlem26  37647  poimirlem28  37649  itgabsnc  37690  fsumshftd  38952  riotasv2s  38958  cdlemefs32sn1aw  40415  mzpsubmpt  42738  mzpsubst  42743  eq0rabdioph  42771  eqrabdioph  42772  rabdiophlem2  42797  fphpd  42811  monotuz  42937  monotoddzz  42939  oddcomabszz  42940  flcidc  43166  binomcxplemdvbinom  44349  binomcxplemdvsum  44351  binomcxplemnotnn0  44352  modelaxreplem3  44977  rfcnnnub  45037  disjinfi  45193  supxrleubrnmptf  45454  caucvgbf  45492  cvgcaule  45494  fsummulc1f  45576  fsumnncl  45577  fsumf1of  45579  fsumreclf  45581  fsumlessf  45582  fsumsermpt  45584  fmul01  45585  fmuldfeqlem1  45587  fmuldfeq  45588  fmul01lt1lem1  45589  fmul01lt1lem2  45590  fprodexp  45599  fprodabs2  45600  fprodcnlem  45604  climmulf  45609  climsuse  45613  climrecf  45614  climaddf  45620  0ellimcdiv  45654  climsubmpt  45665  climfveqf  45685  climinf2mpt  45719  climinfmpt  45720  fprodcncf  45905  dvmptmulf  45942  dvmptfprod  45950  iblspltprt  45978  stoweidlem3  46008  stoweidlem19  46024  stoweidlem22  46027  stoweidlem42  46047  fourierdlem31  46143  fourierdlem86  46197  fourierdlem89  46200  fourierdlem91  46202  fourierdlem112  46223  sge0f1o  46387  sge0lempt  46415  sge0iunmpt  46423  sge0ltfirpmpt2  46431  sge0isummpt2  46437  sge0xaddlem2  46439  sge0xadd  46440  vonhoire  46677  salpreimagelt  46712  smflim  46782  smfresal  46793  smfinflem  46822  eu2ndop1stv  47130