Theorem nfrexw 3286

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 2377. 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 1806	. . 3 ⊢ Ⅎ𝑦⊤
2		nfralw.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3	2	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝐴)
4		nfralw.2	. . . 4 ⊢ Ⅎ𝑥𝜑
5	4	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝜑)
6	1, 3, 5	nfrexdw 3284	. 2 ⊢ (⊤ → Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑)
7	6	mptru 1549	1 ⊢ Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑

Syntax hints:  ⊤wtru 1543  Ⅎwnf 1785  Ⅎwnfc 2884  ∃wrex 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-10 2147  ax-11 2163  ax-12 2185

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-nf 1786  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063

This theorem is referenced by:  nfiun  4966  rexopabb  5477  nffr  5598  abrexex2g  7911  indexfi  9264  nfoi  9423  ixpiunwdom  9499  hsmexlem2  10343  iunfo  10455  iundom2g  10456  reclem2pr  10965  nfwrd  14499  nfsum1  15646  nfsum  15647  nfcprod1  15867  nfcprod  15868  ptclsg  23593  iunmbl2  25537  mbfsup  25644  limciun  25874  opreu2reuALT  32564  iundisjf  32677  xrofsup  32858  locfinreflem  34003  esum2d  34256  bnj873  35085  bnj1014  35122  bnj1123  35147  bnj1307  35184  bnj1445  35205  bnj1446  35206  bnj1467  35215  bnj1463  35216  onvf1odlem2  35305  poimirlem24  37982  poimirlem26  37984  poimirlem27  37985  indexa  38071  filbcmb  38078  sdclem2  38080  sdclem1  38081  fdc1  38084  sbcrexgOLD  43234  rexrabdioph  43243  rexfrabdioph  43244  elnn0rabdioph  43252  dvdsrabdioph  43259  oaun3lem1  43823  modelaxreplem3  45428  modelaxrep  45429  permaxrep  45454  disjrnmpt2  45639  rnmptbdlem  45705  infrnmptle  45872  infxrunb3rnmpt  45877  climinff  46062  xlimmnfv  46283  xlimpnfv  46287  cncfshift  46323  stoweidlem53  46502  stoweidlem57  46506  fourierdlem48  46603  fourierdlem73  46628  sge0gerp  46844  sge0resplit  46855  sge0reuz  46896  meaiuninc3v  46933  smfsup  47263  smfsupmpt  47264  smfinf  47267  smfinfmpt  47268  cbvrex2  47567  2reu8i  47576  mogoldbb  48276