Theorem nfrexw 3313

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 2404. See nfrex 3364 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 1834	. . 3 ⊢ Ⅎ𝑦⊤
2		nfralw.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3	2	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝐴)
4		nfralw.2	. . . 4 ⊢ Ⅎ𝑥𝜑
5	4	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝜑)
6	1, 3, 5	nfrexdw 3311	. 2 ⊢ (⊤ → Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑)
7	6	mptru 1577	1 ⊢ Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑

Syntax hints:  ⊤wtru 1571  Ⅎwnf 1813  Ⅎwnfc 2910  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-10 2176  ax-11 2192  ax-12 2213

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-nf 1814  df-clel 2838  df-nfc 2912  df-ral 3080  df-rex 3090

This theorem is referenced by:  nfiun  4988  rexopabb  5512  nffr  5634  abrexex2g  7957  indexfi  9313  nfoi  9472  ixpiunwdom  9548  hsmexlem2  10406  iunfo  10518  iundom2g  10519  reclem2pr  11028  nfwrd  14576  nfsum1  15737  nfsum  15738  nfcprod1  15958  nfcprod  15959  ptclsg  23772  iunmbl2  25716  mbfsup  25823  limciun  26053  opreu2reuALT  32823  iundisjf  32934  xrofsup  33112  locfinreflem  34230  esum2d  34483  bnj873  35312  bnj1014  35349  bnj1123  35374  bnj1307  35411  bnj1445  35432  bnj1446  35433  bnj1467  35442  bnj1463  35443  onvf1odlem2  35588  poimirlem24  38295  poimirlem26  38297  poimirlem27  38298  indexa  38384  filbcmb  38391  sdclem2  38393  sdclem1  38394  fdc1  38397  rexrabdioph  43521  rexfrabdioph  43522  elnn0rabdioph  43530  dvdsrabdioph  43537  oaun3lem1  44101  modelaxreplem3  45689  modelaxrep  45690  permaxrep  45715  disjrnmpt2  45906  rnmptbdlem  45970  infrnmptle  46137  infxrunb3rnmpt  46142  climinff  46327  xlimmnfv  46548  xlimpnfv  46552  cncfshift  46588  stoweidlem53  46767  stoweidlem57  46771  fourierdlem48  46868  fourierdlem73  46893  sge0gerp  47109  sge0resplit  47120  sge0reuz  47161  meaiuninc3v  47198  smfsup  47528  smfsupmpt  47529  smfinf  47532  smfinfmpt  47533  cbvrex2  47841  2reu8i  47850  mogoldbb  48550  nfrals  50582