Theorem nfrexw 3289

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 2371. See nfrex 3351 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 3286	. 2 ⊢ (⊤ → Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑)
7	6	mptru 1547	1 ⊢ Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑

Syntax hints:  ⊤wtru 1541  Ⅎwnf 1783  Ⅎwnfc 2877  ∃wrex 3054

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 2804  df-nfc 2879  df-ral 3046  df-rex 3055

This theorem is referenced by:  nfiun  4990  rexopabb  5491  nffr  5614  abrexex2g  7946  indexfi  9318  nfoi  9474  ixpiunwdom  9550  hsmexlem2  10387  iunfo  10499  iundom2g  10500  reclem2pr  11008  nfwrd  14515  nfsum1  15663  nfsum  15664  nfcprod1  15881  nfcprod  15882  ptclsg  23509  iunmbl2  25465  mbfsup  25572  limciun  25802  opreu2reuALT  32413  iundisjf  32525  xrofsup  32697  locfinreflem  33837  esum2d  34090  bnj873  34921  bnj1014  34958  bnj1123  34983  bnj1307  35020  bnj1445  35041  bnj1446  35042  bnj1467  35051  bnj1463  35052  onvf1odlem2  35098  poimirlem24  37645  poimirlem26  37647  poimirlem27  37648  indexa  37734  filbcmb  37741  sdclem2  37743  sdclem1  37744  fdc1  37747  sbcrexgOLD  42780  rexrabdioph  42789  rexfrabdioph  42790  elnn0rabdioph  42798  dvdsrabdioph  42805  oaun3lem1  43370  modelaxreplem3  44977  modelaxrep  44978  permaxrep  45003  disjrnmpt2  45189  rnmptbdlem  45256  infrnmptle  45426  infxrunb3rnmpt  45431  climinff  45616  xlimmnfv  45839  xlimpnfv  45843  cncfshift  45879  stoweidlem53  46058  stoweidlem57  46062  fourierdlem48  46159  fourierdlem73  46184  sge0gerp  46400  sge0resplit  46411  sge0reuz  46452  meaiuninc3v  46489  smfsup  46819  smfsupmpt  46820  smfinf  46823  smfinfmpt  46824  cbvrex2  47109  2reu8i  47118  mogoldbb  47790