Theorem nfrexw 3310

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 2374. See nfrex 3372 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 1800	. . 3 ⊢ Ⅎ𝑦⊤
2		nfralw.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3	2	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝐴)
4		nfralw.2	. . . 4 ⊢ Ⅎ𝑥𝜑
5	4	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝜑)
6	1, 3, 5	nfrexdw 3307	. 2 ⊢ (⊤ → Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑)
7	6	mptru 1543	1 ⊢ Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑

Syntax hints:  ⊤wtru 1537  Ⅎwnf 1779  Ⅎwnfc 2887  ∃wrex 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-10 2138  ax-11 2154  ax-12 2174

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1539  df-ex 1776  df-nf 1780  df-clel 2813  df-nfc 2889  df-ral 3059  df-rex 3068

This theorem is referenced by:  nfiun  5027  rexopabb  5537  nffr  5661  abrexex2g  7987  indexfi  9397  nfoi  9551  ixpiunwdom  9627  hsmexlem2  10464  iunfo  10576  iundom2g  10577  reclem2pr  11085  nfwrd  14577  nfsum1  15722  nfsum  15723  nfcprod1  15940  nfcprod  15941  ptclsg  23638  iunmbl2  25605  mbfsup  25712  limciun  25943  opreu2reuALT  32504  iundisjf  32608  xrofsup  32777  locfinreflem  33800  esum2d  34073  bnj873  34916  bnj1014  34953  bnj1123  34978  bnj1307  35015  bnj1445  35036  bnj1446  35037  bnj1467  35046  bnj1463  35047  poimirlem24  37630  poimirlem26  37632  poimirlem27  37633  indexa  37719  filbcmb  37726  sdclem2  37728  sdclem1  37729  fdc1  37732  sbcrexgOLD  42772  rexrabdioph  42781  rexfrabdioph  42782  elnn0rabdioph  42790  dvdsrabdioph  42797  oaun3lem1  43363  modelaxreplem3  44944  modelaxrep  44945  disjrnmpt2  45130  rnmptbdlem  45199  infrnmptle  45372  infxrunb3rnmpt  45377  climinff  45566  xlimmnfv  45789  xlimpnfv  45793  cncfshift  45829  stoweidlem53  46008  stoweidlem57  46012  fourierdlem48  46109  fourierdlem73  46134  sge0gerp  46350  sge0resplit  46361  sge0reuz  46402  meaiuninc3v  46439  smfsup  46769  smfsupmpt  46770  smfinf  46773  smfinfmpt  46774  cbvrex2  47053  2reu8i  47062  mogoldbb  47709