Theorem nfrexw 3277

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 2370. See nfrex 3338 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 1804	. . 3 ⊢ Ⅎ𝑦⊤
2		nfralw.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3	2	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝐴)
4		nfralw.2	. . . 4 ⊢ Ⅎ𝑥𝜑
5	4	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝜑)
6	1, 3, 5	nfrexdw 3275	. 2 ⊢ (⊤ → Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑)
7	6	mptru 1547	1 ⊢ Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑

Syntax hints:  ⊤wtru 1541  Ⅎwnf 1783  Ⅎwnfc 2876  ∃wrex 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-10 2142  ax-11 2158  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-nf 1784  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054

This theorem is referenced by:  nfiun  4973  rexopabb  5471  nffr  5592  abrexex2g  7899  indexfi  9250  nfoi  9406  ixpiunwdom  9482  hsmexlem2  10321  iunfo  10433  iundom2g  10434  reclem2pr  10942  nfwrd  14450  nfsum1  15597  nfsum  15598  nfcprod1  15815  nfcprod  15816  ptclsg  23500  iunmbl2  25456  mbfsup  25563  limciun  25793  opreu2reuALT  32421  iundisjf  32533  xrofsup  32710  locfinreflem  33807  esum2d  34060  bnj873  34891  bnj1014  34928  bnj1123  34953  bnj1307  34990  bnj1445  35011  bnj1446  35012  bnj1467  35021  bnj1463  35022  onvf1odlem2  35081  poimirlem24  37628  poimirlem26  37630  poimirlem27  37631  indexa  37717  filbcmb  37724  sdclem2  37726  sdclem1  37727  fdc1  37730  sbcrexgOLD  42762  rexrabdioph  42771  rexfrabdioph  42772  elnn0rabdioph  42780  dvdsrabdioph  42787  oaun3lem1  43351  modelaxreplem3  44958  modelaxrep  44959  permaxrep  44984  disjrnmpt2  45170  rnmptbdlem  45237  infrnmptle  45406  infxrunb3rnmpt  45411  climinff  45596  xlimmnfv  45819  xlimpnfv  45823  cncfshift  45859  stoweidlem53  46038  stoweidlem57  46042  fourierdlem48  46139  fourierdlem73  46164  sge0gerp  46380  sge0resplit  46391  sge0reuz  46432  meaiuninc3v  46469  smfsup  46799  smfsupmpt  46800  smfinf  46803  smfinfmpt  46804  cbvrex2  47092  2reu8i  47101  mogoldbb  47773