Theorem nfrexw 3305

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 2369. See nfrex 3368 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 1799	. . 3 ⊢ Ⅎ𝑦⊤
2		nfralw.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3	2	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝐴)
4		nfralw.2	. . . 4 ⊢ Ⅎ𝑥𝜑
5	4	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝜑)
6	1, 3, 5	nfrexdw 3302	. 2 ⊢ (⊤ → Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑)
7	6	mptru 1541	1 ⊢ Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑

Syntax hints:  ⊤wtru 1535  Ⅎwnf 1778  Ⅎwnfc 2879  ∃wrex 3063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2102  ax-10 2133  ax-11 2150  ax-12 2170

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1537  df-ex 1775  df-nf 1779  df-clel 2806  df-nfc 2881  df-ral 3055  df-rex 3064

This theorem is referenced by:  nfiun  5036  rexopabb  5538  nffr  5660  abrexex2g  7986  indexfi  9411  nfoi  9564  ixpiunwdom  9640  hsmexlem2  10477  iunfo  10589  iundom2g  10590  reclem2pr  11098  nfwrd  14572  nfsum1  15715  nfsum  15716  nfcprod1  15933  nfcprod  15934  ptclsg  23633  iunmbl2  25600  mbfsup  25707  limciun  25937  opreu2reuALT  32428  iundisjf  32535  xrofsup  32699  locfinreflem  33693  esum2d  33964  bnj873  34807  bnj1014  34844  bnj1123  34869  bnj1307  34906  bnj1445  34927  bnj1446  34928  bnj1467  34937  bnj1463  34938  poimirlem24  37392  poimirlem26  37394  poimirlem27  37395  indexa  37481  filbcmb  37488  sdclem2  37490  sdclem1  37491  fdc1  37494  sbcrexgOLD  42513  rexrabdioph  42522  rexfrabdioph  42523  elnn0rabdioph  42531  dvdsrabdioph  42538  oaun3lem1  43111  disjrnmpt2  44865  rnmptbdlem  44934  infrnmptle  45108  infxrunb3rnmpt  45113  climinff  45302  xlimmnfv  45525  xlimpnfv  45529  cncfshift  45565  stoweidlem53  45744  stoweidlem57  45748  fourierdlem48  45845  fourierdlem73  45870  sge0gerp  46086  sge0resplit  46097  sge0reuz  46138  meaiuninc3v  46175  smfsup  46505  smfsupmpt  46506  smfinf  46509  smfinfmpt  46510  cbvrex2  46787  2reu8i  46796  mogoldbb  47427