Theorem nfrexw 3284

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 2376. See nfrex 3345 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 1805	. . 3 ⊢ Ⅎ𝑦⊤
2		nfralw.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3	2	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝐴)
4		nfralw.2	. . . 4 ⊢ Ⅎ𝑥𝜑
5	4	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝜑)
6	1, 3, 5	nfrexdw 3282	. 2 ⊢ (⊤ → Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑)
7	6	mptru 1548	1 ⊢ Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑

Syntax hints:  ⊤wtru 1542  Ⅎwnf 1784  Ⅎwnfc 2883  ∃wrex 3060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-10 2146  ax-11 2162  ax-12 2184

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-nf 1785  df-clel 2811  df-nfc 2885  df-ral 3052  df-rex 3061

This theorem is referenced by:  nfiun  4978  rexopabb  5476  nffr  5597  abrexex2g  7908  indexfi  9260  nfoi  9419  ixpiunwdom  9495  hsmexlem2  10337  iunfo  10449  iundom2g  10450  reclem2pr  10959  nfwrd  14466  nfsum1  15613  nfsum  15614  nfcprod1  15831  nfcprod  15832  ptclsg  23559  iunmbl2  25514  mbfsup  25621  limciun  25851  opreu2reuALT  32551  iundisjf  32664  xrofsup  32847  locfinreflem  33997  esum2d  34250  bnj873  35080  bnj1014  35117  bnj1123  35142  bnj1307  35179  bnj1445  35200  bnj1446  35201  bnj1467  35210  bnj1463  35211  onvf1odlem2  35298  poimirlem24  37845  poimirlem26  37847  poimirlem27  37848  indexa  37934  filbcmb  37941  sdclem2  37943  sdclem1  37944  fdc1  37947  sbcrexgOLD  43037  rexrabdioph  43046  rexfrabdioph  43047  elnn0rabdioph  43055  dvdsrabdioph  43062  oaun3lem1  43626  modelaxreplem3  45231  modelaxrep  45232  permaxrep  45257  disjrnmpt2  45442  rnmptbdlem  45509  infrnmptle  45677  infxrunb3rnmpt  45682  climinff  45867  xlimmnfv  46088  xlimpnfv  46092  cncfshift  46128  stoweidlem53  46307  stoweidlem57  46311  fourierdlem48  46408  fourierdlem73  46433  sge0gerp  46649  sge0resplit  46660  sge0reuz  46701  meaiuninc3v  46738  smfsup  47068  smfsupmpt  47069  smfinf  47072  smfinfmpt  47073  cbvrex2  47360  2reu8i  47369  mogoldbb  48041