Theorem nfrexw 3286

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 2377. See nfrex 3347 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 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 3284	. 2 ⊢ (⊤ → Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑)
7	6	mptru 1549	1 ⊢ Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑

Syntax hints:  ⊤wtru 1543  Ⅎwnf 1785  Ⅎwnfc 2884  ∃wrex 3062

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-10 2147  ax-11 2163  ax-12 2185

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-nf 1786  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063

This theorem is referenced by:  nfiun  4980  rexopabb  5484  nffr  5605  abrexex2g  7918  indexfi  9272  nfoi  9431  ixpiunwdom  9507  hsmexlem2  10349  iunfo  10461  iundom2g  10462  reclem2pr  10971  nfwrd  14478  nfsum1  15625  nfsum  15626  nfcprod1  15843  nfcprod  15844  ptclsg  23571  iunmbl2  25526  mbfsup  25633  limciun  25863  opreu2reuALT  32563  iundisjf  32676  xrofsup  32858  locfinreflem  34018  esum2d  34271  bnj873  35100  bnj1014  35137  bnj1123  35162  bnj1307  35199  bnj1445  35220  bnj1446  35221  bnj1467  35230  bnj1463  35231  onvf1odlem2  35320  poimirlem24  37895  poimirlem26  37897  poimirlem27  37898  indexa  37984  filbcmb  37991  sdclem2  37993  sdclem1  37994  fdc1  37997  sbcrexgOLD  43142  rexrabdioph  43151  rexfrabdioph  43152  elnn0rabdioph  43160  dvdsrabdioph  43167  oaun3lem1  43731  modelaxreplem3  45336  modelaxrep  45337  permaxrep  45362  disjrnmpt2  45547  rnmptbdlem  45613  infrnmptle  45781  infxrunb3rnmpt  45786  climinff  45971  xlimmnfv  46192  xlimpnfv  46196  cncfshift  46232  stoweidlem53  46411  stoweidlem57  46415  fourierdlem48  46512  fourierdlem73  46537  sge0gerp  46753  sge0resplit  46764  sge0reuz  46805  meaiuninc3v  46842  smfsup  47172  smfsupmpt  47173  smfinf  47176  smfinfmpt  47177  cbvrex2  47464  2reu8i  47473  mogoldbb  48145