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 2410. See nfrex 3371 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 1831	. . 3 ⊢ Ⅎ𝑦⊤
2		nfralw.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3	2	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝐴)
4		nfralw.2	. . . 4 ⊢ Ⅎ𝑥𝜑
5	4	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝜑)
6	1, 3, 5	nfrexdw 3317	. 2 ⊢ (⊤ → Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑)
7	6	mptru 1574	1 ⊢ Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑

Syntax hints:  ⊤wtru 1568  Ⅎwnf 1810  Ⅎwnfc 2916  ∃wrex 3095

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-10 2182  ax-11 2198  ax-12 2219

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-nf 1811  df-clel 2844  df-nfc 2918  df-ral 3086  df-rex 3096

This theorem is referenced by:  nfiun  4992  rexopabb  5513  nffr  5635  abrexex2g  7960  indexfi  9316  nfoi  9475  ixpiunwdom  9551  hsmexlem2  10410  iunfo  10522  iundom2g  10523  reclem2pr  11032  nfwrd  14579  nfsum1  15740  nfsum  15741  nfcprod1  15961  nfcprod  15962  ptclsg  23740  iunmbl2  25684  mbfsup  25791  limciun  26021  opreu2reuALT  32763  iundisjf  32874  xrofsup  33052  locfinreflem  34174  esum2d  34427  bnj873  35256  bnj1014  35293  bnj1123  35318  bnj1307  35355  bnj1445  35376  bnj1446  35377  bnj1467  35386  bnj1463  35387  onvf1odlem2  35486  poimirlem24  38182  poimirlem26  38184  poimirlem27  38185  indexa  38271  filbcmb  38278  sdclem2  38280  sdclem1  38281  fdc1  38284  rexrabdioph  43412  rexfrabdioph  43413  elnn0rabdioph  43421  dvdsrabdioph  43428  oaun3lem1  43992  modelaxreplem3  45580  modelaxrep  45581  permaxrep  45606  disjrnmpt2  45797  rnmptbdlem  45861  infrnmptle  46028  infxrunb3rnmpt  46033  climinff  46218  xlimmnfv  46439  xlimpnfv  46443  cncfshift  46479  stoweidlem53  46658  stoweidlem57  46662  fourierdlem48  46759  fourierdlem73  46784  sge0gerp  47000  sge0resplit  47011  sge0reuz  47052  meaiuninc3v  47089  smfsup  47419  smfsupmpt  47420  smfinf  47423  smfinfmpt  47424  cbvrex2  47729  2reu8i  47738  mogoldbb  48438  nfrals  50466