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

Syntax hints:  ⊤wtru 1542  Ⅎwnf 1785  Ⅎwnfc 2883  ∃wrex 3070

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-10 2137  ax-11 2154  ax-12 2171

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-nf 1786  df-clel 2810  df-nfc 2885  df-ral 3062  df-rex 3071

This theorem is referenced by:  nfiun  5021  rexopabb  5522  nffr  5644  abrexex2g  7935  indexfi  9345  nfoi  9493  ixpiunwdom  9569  hsmexlem2  10406  iunfo  10518  iundom2g  10519  reclem2pr  11027  nfwrd  14477  nfsum1  15620  nfsum  15621  nfcprod1  15838  nfcprod  15839  ptclsg  23050  iunmbl2  25005  mbfsup  25112  limciun  25342  opreu2reuALT  31644  iundisjf  31749  xrofsup  31915  locfinreflem  32715  esum2d  32986  bnj873  33830  bnj1014  33867  bnj1123  33892  bnj1307  33929  bnj1445  33950  bnj1446  33951  bnj1467  33960  bnj1463  33961  poimirlem24  36380  poimirlem26  36382  poimirlem27  36383  indexa  36470  filbcmb  36477  sdclem2  36479  sdclem1  36480  fdc1  36483  sbcrexgOLD  41358  rexrabdioph  41367  rexfrabdioph  41368  elnn0rabdioph  41376  dvdsrabdioph  41383  oaun3lem1  41959  disjrnmpt2  43721  rnmptbdlem  43796  infrnmptle  43970  infxrunb3rnmpt  43975  climinff  44164  xlimmnfv  44387  xlimpnfv  44391  cncfshift  44427  stoweidlem53  44606  stoweidlem57  44610  fourierdlem48  44707  fourierdlem73  44732  sge0gerp  44948  sge0resplit  44959  sge0reuz  45000  meaiuninc3v  45037  smfsup  45367  smfsupmpt  45368  smfinf  45371  smfinfmpt  45372  cbvrex2  45648  2reu8i  45657  mogoldbb  46289