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

Theorem nfel1 2587
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 2577 . 2  |-  F/_ x B
31, 2nfel 2585 1  |-  F/ x  A  e.  B
Colors of variables: wff setvar class
Syntax hints:   F/wnf 1594    e. wcel 1761   F/_wnfc 2564
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-cleq 2434  df-clel 2437  df-nfc 2566
This theorem is referenced by:  vtocl2gf  3029  vtocl3gf  3030  vtoclgaf  3032  vtocl2gaf  3034  vtocl3gaf  3036  nfop  4072  reusv2lem4  4493  reusv2  4495  rabxfrd  4510  pofun  4653  nfse  4691  fvmptf  5787  fmptcof  5874  fliftfuns  6004  riota2f  6072  ovmpt2s  6213  ov2gf  6214  ofmpteq  6337  fmpt2x  6639  offval22  6651  qliftfuns  7183  xpf1o  7469  iunfi  7595  wdom2d  7791  scottex  8088  dfac8clem  8198  ac6num  8644  pwfseqlem4a  8824  pwfseqlem4  8825  gruiin  8973  rlimcld2  13052  summolem3  13187  summolem2a  13188  zsum  13191  fsum  13193  sumss2  13199  fsumcvg2  13200  fsum2dlem  13233  fsumcom2  13237  fsumshftm  13244  fsum0diag2  13246  fsum00  13257  fsumabs  13260  fsumrlim  13270  fsumo1  13271  o1fsum  13272  fsumiun  13280  pcmpt  13950  pcmptdvds  13952  dprdwd  16485  dprdwdOLD  16491  mdetralt2  18374  mdetunilem2  18378  fiuncmp  18966  elptr2  19106  ptcld  19145  ptcnplem  19153  ptcnp  19154  elmptrab  19359  utopsnneiplem  19781  prdsdsf  19901  prdsxmet  19903  fsumcn  20405  ovolfiniun  20943  ovoliunlem3  20946  ovoliun  20947  ovoliun2  20948  finiunmbl  20984  volfiniun  20987  iunmbl  20993  voliun  20994  itgfsum  21263  itgabs  21271  dvmptfsum  21406  dvfsumle  21452  dvfsumabs  21454  dvfsumlem1  21457  dvfsumlem3  21459  dvfsumlem4  21460  dvfsumrlim  21462  dvfsumrlim2  21463  dvfsum2  21465  itgsubst  21480  fsumdvdscom  22484  fsumvma  22511  dchrisumlema  22696  dchrisumlem2  22698  dchrisumlem3  22699  suppss2f  25889  esumcl  26422  esum0  26439  esumcst  26450  esumfsup  26455  measiun  26568  voliune  26581  volfiniune  26582  iota5f  27310  prodmolem3  27375  prodmolem2a  27376  zprod  27379  fprod  27383  prodss  27389  fprodser  27391  fprodm1s  27409  fprodp1s  27410  fprodabs  27413  fprodefsum  27414  fprodn0  27419  fprod2dlem  27420  fprodcom2  27424  itgabsnc  28386  mzpsubmpt  29004  mzpsubst  29010  eq0rabdioph  29040  eqrabdioph  29041  rabdiophlem2  29065  fphpd  29080  monotuz  29207  monotoddzz  29209  oddcomabszz  29210  flcidc  29456  rfcnnnub  29683  fmul01  29686  fmuldfeqlem1  29688  fmuldfeq  29689  fmul01lt1lem1  29690  fmul01lt1lem2  29691  climmulf  29702  climsuse  29706  climrecf  29707  stoweidlem3  29723  stoweidlem19  29739  stoweidlem22  29742  stoweidlem42  29762  eu2ndop1stv  29951  elovmpt2rab  30083  elovmpt2rab1  30084  riotasv2s  32331  cdlemefs32sn1aw  33780
  Copyright terms: Public domain W3C validator