Theorem nfrexw 3293

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 3354 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 3290	. 2 ⊢ (⊤ → Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑)
7	6	mptru 1547	1 ⊢ Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑

Syntax hints:  ⊤wtru 1541  Ⅎwnf 1783  Ⅎwnfc 2883  ∃wrex 3060

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 2007  ax-8 2110  ax-10 2141  ax-11 2157  ax-12 2177

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 2809  df-nfc 2885  df-ral 3052  df-rex 3061

This theorem is referenced by:  nfiun  4999  rexopabb  5503  nffr  5627  abrexex2g  7963  indexfi  9372  nfoi  9528  ixpiunwdom  9604  hsmexlem2  10441  iunfo  10553  iundom2g  10554  reclem2pr  11062  nfwrd  14561  nfsum1  15706  nfsum  15707  nfcprod1  15924  nfcprod  15925  ptclsg  23553  iunmbl2  25510  mbfsup  25617  limciun  25847  opreu2reuALT  32458  iundisjf  32570  xrofsup  32744  locfinreflem  33871  esum2d  34124  bnj873  34955  bnj1014  34992  bnj1123  35017  bnj1307  35054  bnj1445  35075  bnj1446  35076  bnj1467  35085  bnj1463  35086  poimirlem24  37668  poimirlem26  37670  poimirlem27  37671  indexa  37757  filbcmb  37764  sdclem2  37766  sdclem1  37767  fdc1  37770  sbcrexgOLD  42808  rexrabdioph  42817  rexfrabdioph  42818  elnn0rabdioph  42826  dvdsrabdioph  42833  oaun3lem1  43398  modelaxreplem3  45005  modelaxrep  45006  permaxrep  45031  disjrnmpt2  45212  rnmptbdlem  45279  infrnmptle  45450  infxrunb3rnmpt  45455  climinff  45640  xlimmnfv  45863  xlimpnfv  45867  cncfshift  45903  stoweidlem53  46082  stoweidlem57  46086  fourierdlem48  46183  fourierdlem73  46208  sge0gerp  46424  sge0resplit  46435  sge0reuz  46476  meaiuninc3v  46513  smfsup  46843  smfsupmpt  46844  smfinf  46847  smfinfmpt  46848  cbvrex2  47133  2reu8i  47142  mogoldbb  47799