Theorem nfrexw 3292

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 nfrexg 3340 for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 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 3289	. 2 ⊢ (⊤ → Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑)
7	6	mptru 1546	1 ⊢ Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑

Syntax hints:  ⊤wtru 1540  Ⅎwnf 1783  Ⅎwnfc 2884  ∃wrex 3070

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-10 2135  ax-11 2152  ax-12 2169

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-tru 1542  df-ex 1780  df-nf 1784  df-clel 2814  df-nfc 2886  df-ral 3062  df-rex 3071

This theorem is referenced by:  nfiun  4961  rexopabb  5454  nffr  5574  abrexex2g  7839  indexfi  9175  nfoi  9321  ixpiunwdom  9397  hsmexlem2  10233  iunfo  10345  iundom2g  10346  reclem2pr  10854  nfwrd  14295  nfsum1  15450  nfsum  15451  nfsumOLD  15452  nfcprod1  15669  nfcprod  15670  ptclsg  22815  iunmbl2  24770  mbfsup  24877  limciun  25107  opreu2reuALT  30874  iundisjf  30977  xrofsup  31139  locfinreflem  31839  esum2d  32110  bnj873  32953  bnj1014  32990  bnj1123  33015  bnj1307  33052  bnj1445  33073  bnj1446  33074  bnj1467  33083  bnj1463  33084  poimirlem24  35849  poimirlem26  35851  poimirlem27  35852  indexa  35939  filbcmb  35946  sdclem2  35948  sdclem1  35949  fdc1  35952  sbcrexgOLD  40802  rexrabdioph  40811  rexfrabdioph  40812  elnn0rabdioph  40820  dvdsrabdioph  40827  disjrnmpt2  42946  rnmptbdlem  43022  infrnmptle  43191  infxrunb3rnmpt  43196  climinff  43381  xlimmnfv  43604  xlimpnfv  43608  cncfshift  43644  stoweidlem53  43823  stoweidlem57  43827  fourierdlem48  43924  fourierdlem73  43949  sge0gerp  44163  sge0resplit  44174  sge0reuz  44215  meaiuninc3v  44252  smfsup  44582  smfsupmpt  44583  smfinf  44586  smfinfmpt  44587  cbvrex2  44840  2reu8i  44849  mogoldbb  45481