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

Step	Hyp	Ref	Expression
1		nftru 1626	. . 3
2		nfrex.1	. . . 4
3	2	a1i 11	. . 3
4		nfrex.2	. . . 4
5	4	a1i 11	. . 3
6	1, 3, 5	nfrexd 2919	. 2
7	6	trud 1404	1

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