Theorem nfrex 2990

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 1721	. . 3 ⊢ Ⅎ𝑦⊤
2		nfrex.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3	2	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝐴)
4		nfrex.2	. . . 4 ⊢ Ⅎ𝑥𝜑
5	4	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝜑)
6	1, 3, 5	nfrexd 2989	. 2 ⊢ (⊤ → Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑)
7	6	trud 1484	1 ⊢ Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑

Syntax hints:  ⊤wtru 1476  Ⅎwnf 1699  Ⅎwnfc 2738  ∃wrex 2897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902

This theorem is referenced by:  r19.12  3045  nfuni  4378  rabasiun  4459  nfiun  4484  nffr  5012  abrexex2g  7036  abrexex2  7040  indexfi  8157  nfoi  8302  ixpiunwdom  8379  hsmexlem2  9132  iunfo  9240  iundom2g  9241  reclem2pr  9749  nfwrd  13188  nfsum1  14268  nfsum  14269  nfcprod1  14479  nfcprod  14480  ptclsg  21228  iunmbl2  23132  mbfsup  23237  limciun  23464  iundisjf  28784  xrofsup  28923  locfinreflem  29235  esum2d  29482  bnj873  30248  bnj1014  30284  bnj1123  30308  bnj1307  30345  bnj1445  30366  bnj1446  30367  bnj1467  30376  bnj1463  30377  poimirlem24  32603  poimirlem26  32605  poimirlem27  32606  indexa  32698  filbcmb  32705  sdclem2  32708  sdclem1  32709  fdc1  32712  sbcrexgOLD  36367  rexrabdioph  36376  rexfrabdioph  36377  elnn0rabdioph  36385  dvdsrabdioph  36392  disjrnmpt2  38370  climinff  38678  cncfshift  38759  stoweidlem53  38946  stoweidlem57  38950  fourierdlem48  39047  fourierdlem73  39072  sge0gerp  39288  sge0resplit  39299  sge0reuz  39340  cbvrex2  39822