Theorem nfrexw 3310

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

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

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 2147  ax-10 2178  ax-11 2194  ax-12 2213

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 2835  df-nfc 2909  df-ral 3077  df-rex 3087

This theorem is used by:  nfiun  4982  rexopabb  5506  nffr  5628  abrexex2g  7962  indexfi  9328  nfoi  9487  ixpiunwdom  9563  hsmexlem2  10430  iunfo  10548  iundom2g  10549  reclem2pr  11058  nfwrd  14609  nfsum1  15778  nfsum  15779  nfcprod1  15998  nfcprod  15999  ptclsg  23842  iunmbl2  25786  mbfsup  25893  limciun  26122  opreu2reuALT  32953  iundisjf  33063  xrofsup  33239  locfinreflem  34351  esum2d  34604  bnj873  35434  bnj1014  35471  bnj1123  35496  bnj1307  35533  bnj1445  35554  bnj1446  35555  bnj1467  35564  bnj1463  35565  onvf1odlem2  35702  poimirlem24  38394  poimirlem26  38396  poimirlem27  38397  indexa  38484  filbcmb  38491  sdclem2  38493  sdclem1  38494  fdc1  38497  rexrabdioph  43636  rexfrabdioph  43637  elnn0rabdioph  43645  dvdsrabdioph  43652  oaun3lem1  44216  modelaxreplem3  45804  modelaxrep  45805  permaxrep  45830  disjrnmpt2  46021  rnmptbdlem  46085  infrnmptle  46252  infxrunb3rnmpt  46257  climinff  46442  xlimmnfv  46663  xlimpnfv  46667  cncfshift  46703  stoweidlem53  46882  stoweidlem57  46886  fourierdlem48  46983  fourierdlem73  47008  sge0gerp  47224  sge0resplit  47235  sge0reuz  47276  meaiuninc3v  47313  smfsup  47643  smfsupmpt  47644  smfinf  47647  smfinfmpt  47648  cbvrex2  47993  2reu8i  48002  mogoldbb  48702  nfrals  50734