Theorem nfrexw 3315

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 2406. See nfrex 3366 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 3313	. 2 ⊢ (⊤ → Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑)
7	6	mptru 1577	1 ⊢ Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑

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

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 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-10 2179  ax-11 2195  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 2840  df-nfc 2914  df-ral 3082  df-rex 3092

This theorem is used by:  nfiun  4990  rexopabb  5514  nffr  5636  abrexex2g  7967  indexfi  9324  nfoi  9483  ixpiunwdom  9559  hsmexlem2  10426  iunfo  10538  iundom2g  10539  reclem2pr  11048  nfwrd  14598  nfsum1  15765  nfsum  15766  nfcprod1  15985  nfcprod  15986  ptclsg  23823  iunmbl2  25767  mbfsup  25874  limciun  26104  opreu2reuALT  32894  iundisjf  33005  xrofsup  33182  locfinreflem  34294  esum2d  34547  bnj873  35377  bnj1014  35414  bnj1123  35439  bnj1307  35476  bnj1445  35497  bnj1446  35498  bnj1467  35507  bnj1463  35508  onvf1odlem2  35645  poimirlem24  38352  poimirlem26  38354  poimirlem27  38355  indexa  38442  filbcmb  38449  sdclem2  38451  sdclem1  38452  fdc1  38455  rexrabdioph  43579  rexfrabdioph  43580  elnn0rabdioph  43588  dvdsrabdioph  43595  oaun3lem1  44159  modelaxreplem3  45747  modelaxrep  45748  permaxrep  45773  disjrnmpt2  45964  rnmptbdlem  46028  infrnmptle  46195  infxrunb3rnmpt  46200  climinff  46385  xlimmnfv  46606  xlimpnfv  46610  cncfshift  46646  stoweidlem53  46825  stoweidlem57  46829  fourierdlem48  46926  fourierdlem73  46951  sge0gerp  47167  sge0resplit  47178  sge0reuz  47219  meaiuninc3v  47256  smfsup  47586  smfsupmpt  47587  smfinf  47590  smfinfmpt  47591  cbvrex2  47899  2reu8i  47908  mogoldbb  48608  nfrals  50639