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

Theorem nfrex 2917
Description: Bound-variable hypothesis builder for restricted quantification. (Contributed by NM, 1-Sep-1999.) (Revised by Mario Carneiro, 7-Oct-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2019.)
Hypotheses
Ref Expression
nfrex.1  |-  F/_ x A
nfrex.2  |-  F/ x ph
Assertion
Ref Expression
nfrex  |-  F/ x E. y  e.  A  ph

Proof of Theorem nfrex
StepHypRef Expression
1 nftru 1631 . . 3  |-  F/ y T.
2 nfrex.1 . . . 4  |-  F/_ x A
32a1i 11 . . 3  |-  ( T. 
->  F/_ x A )
4 nfrex.2 . . . 4  |-  F/ x ph
54a1i 11 . . 3  |-  ( T. 
->  F/ x ph )
61, 3, 5nfrexd 2916 . 2  |-  ( T. 
->  F/ x E. y  e.  A  ph )
76trud 1407 1  |-  F/ x E. y  e.  A  ph
Colors of variables: wff setvar class
Syntax hints:   T. wtru 1399   F/wnf 1621   F/_wnfc 2602   E.wrex 2805
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ral 2809  df-rex 2810
This theorem is referenced by:  r19.12  2980  nfuni  4241  rabasiun  4319  nfiun  4343  nffr  4842  abrexex2g  6750  abrexex2  6754  nfrecs  7036  indexfi  7820  nfoi  7931  ixpiunwdom  8009  hsmexlem2  8798  iunfo  8905  iundom2g  8906  reclem2pr  9415  nfwrd  12557  nfsum1  13594  nfsum  13595  nfcprod1  13799  nfcprod  13800  ptclsg  20282  iunmbl2  22133  mbfsup  22237  limciun  22464  iundisjf  27659  xrofsup  27816  locfinreflem  28078  esum2d  28322  indexa  30464  filbcmb  30471  sdclem2  30475  sdclem1  30476  fdc1  30479  sbcrexgOLD  30958  rexrabdioph  30967  rexfrabdioph  30968  elnn0rabdioph  30976  dvdsrabdioph  30983  infrglb  31823  climinff  31856  cncfshift  31915  stoweidlem53  32074  stoweidlem57  32078  fourierdlem48  32176  fourierdlem73  32201  cbvrex2  32417  bnj873  34383  bnj1014  34419  bnj1123  34443  bnj1307  34480  bnj1445  34501  bnj1446  34502  bnj1467  34511  bnj1463  34512
  Copyright terms: Public domain W3C validator