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

Theorem nfrex 2827
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 1671 . . 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 2826 . 2  |-  ( T. 
->  F/ x E. y  e.  A  ph )
76trud 1446 1  |-  F/ x E. y  e.  A  ph
Colors of variables: wff setvar class
Syntax hints:   T. wtru 1438   F/wnf 1661   F/_wnfc 2556   E.wrex 2715
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-cleq 2421  df-clel 2424  df-nfc 2558  df-ral 2719  df-rex 2720
This theorem is referenced by:  r19.12  2893  nfuni  4168  rabasiun  4246  nfiun  4270  nffr  4770  abrexex2g  6728  abrexex2  6732  indexfi  7835  nfoi  7982  ixpiunwdom  8059  hsmexlem2  8808  iunfo  8915  iundom2g  8916  reclem2pr  9424  nfwrd  12643  nfsum1  13699  nfsum  13700  nfcprod1  13907  nfcprod  13908  ptclsg  20572  iunmbl2  22452  mbfsup  22562  limciun  22791  iundisjf  28145  xrofsup  28303  locfinreflem  28619  esum2d  28866  bnj873  29687  bnj1014  29723  bnj1123  29747  bnj1307  29784  bnj1445  29805  bnj1446  29806  bnj1467  29815  bnj1463  29816  poimirlem24  31871  poimirlem26  31873  poimirlem27  31874  indexa  31967  filbcmb  31974  sdclem2  31978  sdclem1  31979  fdc1  31982  sbcrexgOLD  35540  rexrabdioph  35549  rexfrabdioph  35550  elnn0rabdioph  35558  dvdsrabdioph  35565  disjrnmpt2  37367  infrglbOLD  37552  climinff  37573  climinffOLD  37574  cncfshift  37634  stoweidlem53  37797  stoweidlem57  37801  fourierdlem48  37901  fourierdlem73  37926  sge0gerp  38088  sge0resplit  38099  cbvrex2  38408
  Copyright terms: Public domain W3C validator