Theorem nfrexw 3282

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

Syntax hints:  ⊤wtru 1542  Ⅎwnf 1784  Ⅎwnfc 2881  ∃wrex 3058

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-10 2146  ax-11 2162  ax-12 2182

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-nf 1785  df-clel 2809  df-nfc 2883  df-ral 3050  df-rex 3059

This theorem is referenced by:  nfiun  4976  rexopabb  5474  nffr  5595  abrexex2g  7906  indexfi  9258  nfoi  9417  ixpiunwdom  9493  hsmexlem2  10335  iunfo  10447  iundom2g  10448  reclem2pr  10957  nfwrd  14464  nfsum1  15611  nfsum  15612  nfcprod1  15829  nfcprod  15830  ptclsg  23557  iunmbl2  25512  mbfsup  25619  limciun  25849  opreu2reuALT  32500  iundisjf  32613  xrofsup  32796  locfinreflem  33946  esum2d  34199  bnj873  35029  bnj1014  35066  bnj1123  35091  bnj1307  35128  bnj1445  35149  bnj1446  35150  bnj1467  35159  bnj1463  35160  onvf1odlem2  35247  poimirlem24  37784  poimirlem26  37786  poimirlem27  37787  indexa  37873  filbcmb  37880  sdclem2  37882  sdclem1  37883  fdc1  37886  sbcrexgOLD  42969  rexrabdioph  42978  rexfrabdioph  42979  elnn0rabdioph  42987  dvdsrabdioph  42994  oaun3lem1  43558  modelaxreplem3  45163  modelaxrep  45164  permaxrep  45189  disjrnmpt2  45374  rnmptbdlem  45441  infrnmptle  45609  infxrunb3rnmpt  45614  climinff  45799  xlimmnfv  46020  xlimpnfv  46024  cncfshift  46060  stoweidlem53  46239  stoweidlem57  46243  fourierdlem48  46340  fourierdlem73  46365  sge0gerp  46581  sge0resplit  46592  sge0reuz  46633  meaiuninc3v  46670  smfsup  47000  smfsupmpt  47001  smfinf  47004  smfinfmpt  47005  cbvrex2  47292  2reu8i  47301  mogoldbb  47973