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

Theorem nfel1 2584
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 2574 . 2  |-  F/_ x B
31, 2nfel 2582 1  |-  F/ x  A  e.  B
Colors of variables: wff set class
Syntax hints:   F/wnf 1554    e. wcel 1726   F/_wnfc 2561
This theorem is referenced by:  vtocl2gf  3015  vtocl3gf  3016  vtoclgaf  3018  vtocl2gaf  3020  vtocl3gaf  3022  nfop  4002  pofun  4521  nfse  4559  reusv2lem4  4729  reusv2  4731  rabxfrd  4746  fvmptf  5823  fmptcof  5904  fliftfuns  6038  ovmpt2s  6199  ov2gf  6200  fmpt2x  6419  riota2f  6573  riotasv2s  6598  qliftfuns  6993  xpf1o  7271  iunfi  7396  wdom2d  7550  scottex  7811  dfac8clem  7915  ac6num  8361  pwfseqlem4a  8538  pwfseqlem4  8539  gruiin  8687  rlimcld2  12374  summolem3  12510  summolem2a  12511  zsum  12514  fsum  12516  sumss2  12522  fsumcvg2  12523  fsum2dlem  12556  fsumcom2  12560  fsumshftm  12566  fsum0diag2  12568  fsum00  12579  fsumabs  12582  fsumrlim  12592  fsumo1  12593  o1fsum  12594  fsumiun  12602  pcmpt  13263  pcmptdvds  13265  dprdwd  15571  fiuncmp  17469  elptr2  17608  ptcld  17647  ptcnplem  17655  ptcnp  17656  elmptrab  17861  utopsnneiplem  18279  prdsdsf  18399  prdsxmet  18401  fsumcn  18902  ovolfiniun  19399  ovoliunlem3  19402  ovoliun  19403  ovoliun2  19404  finiunmbl  19440  volfiniun  19443  iunmbl  19449  voliun  19450  itgfsum  19720  itgabs  19728  dvmptfsum  19861  dvfsumle  19907  dvfsumabs  19909  dvfsumlem1  19912  dvfsumlem3  19914  dvfsumlem4  19915  dvfsumrlim  19917  dvfsumrlim2  19918  dvfsum2  19920  itgsubst  19935  fsumdvdscom  20972  fsumvma  20999  dchrisumlema  21184  dchrisumlem2  21186  dchrisumlem3  21187  suppss2f  24051  esumcl  24429  esum0  24446  esumcst  24457  esumfsup  24462  measiun  24574  voliune  24587  volfiniune  24588  iota5f  25184  prodmolem3  25261  prodmolem2a  25262  zprod  25265  fprod  25269  prodss  25275  fprodser  25277  fprodm1s  25295  fprodp1s  25296  fprodabs  25299  fprodefsum  25300  fprodn0  25305  fprod2dlem  25306  fprodcom2  25310  itgabsnc  26276  ofmpteq  26778  mzpsubmpt  26802  mzpsubst  26807  eq0rabdioph  26837  eqrabdioph  26838  rabdiophlem2  26864  fphpd  26879  monotuz  27006  monotoddzz  27008  oddcomabszz  27009  flcidc  27358  rfcnnnub  27685  fmul01  27688  fmuldfeqlem1  27690  fmuldfeq  27691  fmul01lt1lem1  27692  fmul01lt1lem2  27693  climmulf  27708  climsuse  27712  climrecf  27713  stoweidlem3  27730  stoweidlem19  27746  stoweidlem22  27749  stoweidlem42  27769  eu2ndop1stv  27958  elovmpt2rab  28092  elovmpt2rab1  28093  ovmpt3rab1  28094  cdlemefs32sn1aw  31273
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-cleq 2431  df-clel 2434  df-nfc 2563
  Copyright terms: Public domain W3C validator