MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfel1 Structured version   Unicode version

Theorem nfel1 2645
Description: Hypothesis builder for elementhood, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
Hypothesis
Ref Expression
nfeq1.1  |-  F/_ x A
Assertion
Ref Expression
nfel1  |-  F/ x  A  e.  B
Distinct variable group:    x, B
Allowed substitution hint:    A( x)

Proof of Theorem nfel1
StepHypRef Expression
1 nfeq1.1 . 2  |-  F/_ x A
2 nfcv 2629 . 2  |-  F/_ x B
31, 2nfel 2642 1  |-  F/ x  A  e.  B
Colors of variables: wff setvar class
Syntax hints:   F/wnf 1599    e. wcel 1767   F/_wnfc 2615
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-cleq 2459  df-clel 2462  df-nfc 2617
This theorem is referenced by:  vtocl2gf  3173  vtocl3gf  3174  vtoclgaf  3176  vtocl2gaf  3178  vtocl3gaf  3180  nfop  4229  reusv2lem4  4651  reusv2  4653  rabxfrd  4668  pofun  4816  nfse  4854  fvmptf  5964  fmptcof  6053  fliftfuns  6198  riota2f  6265  ovmpt2s  6408  ov2gf  6409  elovmpt2rab  6503  elovmpt2rab1  6504  ofmpteq  6540  fmpt2x  6847  offval22  6859  fvmpt2curryd  6997  qliftfuns  7395  xpf1o  7676  iunfi  7804  wdom2d  8002  scottex  8299  dfac8clem  8409  ac6num  8855  pwfseqlem4a  9035  pwfseqlem4  9036  gruiin  9184  rlimcld2  13360  summolem3  13495  summolem2a  13496  zsum  13499  fsum  13501  sumss2  13507  fsumcvg2  13508  fsum2dlem  13544  fsumcom2  13548  fsumshftm  13555  fsum0diag2  13557  fsum00  13571  fsumabs  13574  fsumrlim  13584  fsumo1  13585  o1fsum  13586  fsumiun  13594  pcmpt  14266  pcmptdvds  14268  dprdwd  16835  dprdwdOLD  16841  gsumply1eq  18118  mdetralt2  18878  mdetunilem2  18882  fiuncmp  19670  elptr2  19810  ptcld  19849  ptcnplem  19857  ptcnp  19858  elmptrab  20063  utopsnneiplem  20485  prdsdsf  20605  prdsxmet  20607  fsumcn  21109  ovolfiniun  21647  ovoliunlem3  21650  ovoliun  21651  ovoliun2  21652  finiunmbl  21689  volfiniun  21692  iunmbl  21698  voliun  21699  itgfsum  21968  itgabs  21976  dvmptfsum  22111  dvfsumle  22157  dvfsumabs  22159  dvfsumlem1  22162  dvfsumlem3  22164  dvfsumlem4  22165  dvfsumrlim  22167  dvfsumrlim2  22168  dvfsum2  22170  itgsubst  22185  fsumdvdscom  23189  fsumvma  23216  dchrisumlema  23401  dchrisumlem2  23403  dchrisumlem3  23404  suppss2f  27150  esumcl  27683  esum0  27700  esumcst  27711  esumfsup  27716  measiun  27829  voliune  27841  volfiniune  27842  iota5f  28577  prodmolem3  28642  prodmolem2a  28643  zprod  28646  fprod  28650  prodss  28656  fprodser  28658  fprodm1s  28676  fprodp1s  28677  fprodabs  28680  fprodefsum  28681  fprodn0  28686  fprod2dlem  28687  fprodcom2  28691  itgabsnc  29661  mzpsubmpt  30279  mzpsubst  30285  eq0rabdioph  30314  eqrabdioph  30315  rabdiophlem2  30339  fphpd  30354  monotuz  30481  monotoddzz  30483  oddcomabszz  30484  flcidc  30728  rfcnnnub  30989  fmul01  31130  fmuldfeqlem1  31132  fmuldfeq  31133  fmul01lt1lem1  31134  fmul01lt1lem2  31135  climmulf  31146  climsuse  31150  climrecf  31151  0ellimcdiv  31191  stoweidlem3  31303  stoweidlem19  31319  stoweidlem22  31322  stoweidlem42  31342  fourierdlem31  31438  fourierdlem86  31493  eu2ndop1stv  31674  fsumshftd  33754  fsumshftdOLD  33755  riotasv2s  33761  cdlemefs32sn1aw  35210
  Copyright terms: Public domain W3C validator