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

Theorem nfrex 2920
 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
nfrex.2
Assertion
Ref Expression
nfrex

Proof of Theorem nfrex
StepHypRef Expression
1 nftru 1626 . . 3
2 nfrex.1 . . . 4
32a1i 11 . . 3
4 nfrex.2 . . . 4
54a1i 11 . . 3
61, 3, 5nfrexd 2919 . 2
76trud 1404 1
 Colors of variables: wff setvar class Syntax hints:   wtru 1396  F/wnf 1616  F/_wnfc 2605  E.wrex 2808 This theorem is referenced by:  r19.12  2983  sbcrexgOLD  3413  nfuni  4255  rabasiun  4334  nfiun  4358  nffr  4858  abrexex2g  6777  abrexex2  6781  nfrecs  7063  indexfi  7848  nfoi  7960  ixpiunwdom  8038  hsmexlem2  8828  iunfo  8935  iundom2g  8936  reclem2pr  9447  nfwrd  12569  nfsum1  13512  nfsum  13513  nfcprod1  13717  nfcprod  13718  ptclsg  20116  iunmbl2  21967  mbfsup  22071  limciun  22298  iundisjf  27448  xrofsup  27582  locfinreflem  27843  indexa  30224  filbcmb  30231  sdclem2  30235  sdclem1  30236  fdc1  30239  rexrabdioph  30727  rexfrabdioph  30728  elnn0rabdioph  30736  dvdsrabdioph  30743  infrglb  31584  climinff  31617  cncfshift  31676  stoweidlem53  31835  stoweidlem57  31839  fourierdlem48  31937  fourierdlem73  31962  cbvrex2  32178  bnj873  33982  bnj1014  34018  bnj1123  34042  bnj1307  34079  bnj1445  34100  bnj1446  34101  bnj1467  34110  bnj1463  34111 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435 This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812  df-rex 2813
 Copyright terms: Public domain W3C validator