Theorem nfrexw 3319

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.) Add disjoint variable condition to avoid ax-13 2380. See nfrex 3383 for a less restrictive version requiring more axioms. (Revised by GG, 20-Jan-2024.)

Hypotheses

Ref	Expression
nfralw.1	⊢ Ⅎ𝑥𝐴
nfralw.2	⊢ Ⅎ𝑥𝜑

Assertion

Ref	Expression
nfrexw	⊢ Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑

Distinct variable group:   𝑥,𝑦

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐴(𝑥,𝑦)

Proof of Theorem nfrexw

Step	Hyp	Ref	Expression
1		nftru 1802	. . 3 ⊢ Ⅎ𝑦⊤
2		nfralw.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3	2	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝐴)
4		nfralw.2	. . . 4 ⊢ Ⅎ𝑥𝜑
5	4	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝜑)
6	1, 3, 5	nfrexdw 3316	. 2 ⊢ (⊤ → Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑)
7	6	mptru 1544	1 ⊢ Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑

Syntax hints:  ⊤wtru 1538  Ⅎwnf 1781  Ⅎwnfc 2893  ∃wrex 3076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-10 2141  ax-11 2158  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-nf 1782  df-clel 2819  df-nfc 2895  df-ral 3068  df-rex 3077

This theorem is referenced by:  nfiun  5046  rexopabb  5547  nffr  5673  abrexex2g  8005  indexfi  9430  nfoi  9583  ixpiunwdom  9659  hsmexlem2  10496  iunfo  10608  iundom2g  10609  reclem2pr  11117  nfwrd  14591  nfsum1  15738  nfsum  15739  nfcprod1  15956  nfcprod  15957  ptclsg  23644  iunmbl2  25611  mbfsup  25718  limciun  25949  opreu2reuALT  32505  iundisjf  32611  xrofsup  32774  locfinreflem  33786  esum2d  34057  bnj873  34900  bnj1014  34937  bnj1123  34962  bnj1307  34999  bnj1445  35020  bnj1446  35021  bnj1467  35030  bnj1463  35031  poimirlem24  37604  poimirlem26  37606  poimirlem27  37607  indexa  37693  filbcmb  37700  sdclem2  37702  sdclem1  37703  fdc1  37706  sbcrexgOLD  42741  rexrabdioph  42750  rexfrabdioph  42751  elnn0rabdioph  42759  dvdsrabdioph  42766  oaun3lem1  43336  disjrnmpt2  45095  rnmptbdlem  45164  infrnmptle  45338  infxrunb3rnmpt  45343  climinff  45532  xlimmnfv  45755  xlimpnfv  45759  cncfshift  45795  stoweidlem53  45974  stoweidlem57  45978  fourierdlem48  46075  fourierdlem73  46100  sge0gerp  46316  sge0resplit  46327  sge0reuz  46368  meaiuninc3v  46405  smfsup  46735  smfsupmpt  46736  smfinf  46739  smfinfmpt  46740  cbvrex2  47019  2reu8i  47028  mogoldbb  47659