Theorem nfrex 3007

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

Step	Hyp	Ref	Expression
1		nftru 1730	. . 3 |- F/ y T.
2		nfrex.1	. . . 4 |- F/_ x A
3	2	a1i 11	. . 3 |- ( T. -> F/_ x A )
4		nfrex.2	. . . 4 |- F/ x ph
5	4	a1i 11	. . 3 |- ( T. -> F/ x ph )
6	1, 3, 5	nfrexd 3006	. 2 |- ( T. -> F/ x E. y e. A ph )
7	6	trud 1493	1 |- F/ x E. y e. A ph

Syntax hints:   T. wtru 1484   F/wnf 1708   F/_wnfc 2751   E.wrex 2913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918

This theorem is referenced by:  r19.12  3063  nfuni  4442  nfiun  4548  nffr  5088  abrexex2g  7144  abrexex2OLD  7150  indexfi  8274  nfoi  8419  ixpiunwdom  8496  hsmexlem2  9249  iunfo  9361  iundom2g  9362  reclem2pr  9870  nfwrd  13333  nfsum1  14420  nfsum  14421  nfcprod1  14640  nfcprod  14641  ptclsg  21418  iunmbl2  23325  mbfsup  23431  limciun  23658  iundisjf  29402  xrofsup  29533  locfinreflem  29907  esum2d  30155  bnj873  30994  bnj1014  31030  bnj1123  31054  bnj1307  31091  bnj1445  31112  bnj1446  31113  bnj1467  31122  bnj1463  31123  poimirlem24  33433  poimirlem26  33435  poimirlem27  33436  indexa  33528  filbcmb  33535  sdclem2  33538  sdclem1  33539  fdc1  33542  sbcrexgOLD  37349  rexrabdioph  37358  rexfrabdioph  37359  elnn0rabdioph  37367  dvdsrabdioph  37374  disjrnmpt2  39375  rnmptbdlem  39470  infrnmptle  39650  infxrunb3rnmpt  39655  climinff  39843  xlimmnfv  40060  xlimpnfv  40064  cncfshift  40087  stoweidlem53  40270  stoweidlem57  40274  fourierdlem48  40371  fourierdlem73  40396  sge0gerp  40612  sge0resplit  40623  sge0reuz  40664  smfsup  41020  smfsupmpt  41021  smfinf  41024  smfinfmpt  41025  cbvrex2  41173  mogoldbb  41673