Theorem nfrexw 3314

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 2404. See nfrex 3364 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 1837	. . 3 ⊢ Ⅎ𝑦⊤
2		nfralw.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3	2	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝐴)
4		nfralw.2	. . . 4 ⊢ Ⅎ𝑥𝜑
5	4	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝜑)
6	1, 3, 5	nfrexdw 3312	. 2 ⊢ (⊤ → Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑)
7	6	mptru 1577	1 ⊢ Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑

This proof depends on syntax axioms:  ⊤wtru 1571  Ⅎwnf 1816  Ⅎwnfc 2911  ∃wrex 3090

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-10 2180  ax-11 2197  ax-12 2216

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-nf 1817  df-clel 2839  df-nfc 2913  df-ral 3081  df-rex 3091

This theorem is used by:  nfiun  4987  rexopabb  5509  nffr  5631  abrexex2g  8010  indexfi  9387  nfoi  9545  ixpiunwdom  9621  hsmexlem2  10544  iunfo  10662  iundom2g  10663  reclem2pr  11172  nfwrd  14729  nfsum1  15901  nfsum  15902  nfcprod1  16121  nfcprod  16122  ptclsg  23989  iunmbl2  25933  mbfsup  26040  limciun  26269  opreu2reuALT  33172  iundisjf  33281  xrofsup  33455  locfinreflem  34583  esum2d  34836  bnj873  35665  bnj1014  35702  bnj1123  35727  bnj1307  35764  bnj1445  35785  bnj1446  35786  bnj1467  35795  bnj1463  35796  rmo6  35821  onvf1odlem2  36073  srepdf  36128  poimirlem24  38830  poimirlem26  38832  poimirlem27  38833  indexa  38935  filbcmb  38940  sdclem2  38942  sdclem1  38943  fdc1  38946  rexrabdioph  44067  rexfrabdioph  44068  elnn0rabdioph  44076  dvdsrabdioph  44083  oaun3lem1  44637  modelaxreplem3  46234  modelaxrep  46235  permaxrep  46260  disjrnmpt2  46476  rnmptbdlem  46540  infrnmptle  46706  infxrunb3rnmpt  46711  climinff  46896  xlimmnfv  47117  xlimpnfv  47121  cncfshift  47157  stoweidlem53  47336  stoweidlem57  47340  fourierdlem48  47437  fourierdlem73  47462  sge0gerp  47678  sge0resplit  47689  sge0reuz  47730  meaiuninc3v  47767  smfsup  48097  smfsupmpt  48098  smfinf  48101  smfinfmpt  48102  cbvrex2  48448  2reu8i  48457  mogoldbb  49156  nfrals  51328