Theorem nfrexw 3287

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 2380. See nfrex 3339 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 1811	. . 3 ⊢ Ⅎ𝑦⊤
2		nfralw.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3	2	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝐴)
4		nfralw.2	. . . 4 ⊢ Ⅎ𝑥𝜑
5	4	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝜑)
6	1, 3, 5	nfrexdw 3285	. 2 ⊢ (⊤ → Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑)
7	6	mptru 1554	1 ⊢ Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑

Syntax hints:  ⊤wtru 1548  Ⅎwnf 1790  Ⅎwnfc 2886  ∃wrex 3063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-10 2152  ax-11 2168  ax-12 2189

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-nf 1791  df-clel 2814  df-nfc 2888  df-ral 3054  df-rex 3064

This theorem is referenced by:  nfiun  4953  rexopabb  5470  nffr  5591  abrexex2g  7906  indexfi  9260  nfoi  9419  ixpiunwdom  9495  hsmexlem2  10340  iunfo  10452  iundom2g  10453  reclem2pr  10962  nfwrd  14496  nfsum1  15643  nfsum  15644  nfcprod1  15864  nfcprod  15865  ptclsg  23598  iunmbl2  25542  mbfsup  25649  limciun  25879  opreu2reuALT  32564  iundisjf  32678  xrofsup  32859  locfinreflem  34024  esum2d  34277  bnj873  35106  bnj1014  35143  bnj1123  35168  bnj1307  35205  bnj1445  35226  bnj1446  35227  bnj1467  35236  bnj1463  35237  onvf1odlem2  35332  poimirlem24  38011  poimirlem26  38013  poimirlem27  38014  indexa  38100  filbcmb  38107  sdclem2  38109  sdclem1  38110  fdc1  38113  rexrabdioph  43239  rexfrabdioph  43240  elnn0rabdioph  43248  dvdsrabdioph  43255  oaun3lem1  43819  modelaxreplem3  45424  modelaxrep  45425  permaxrep  45450  disjrnmpt2  45635  rnmptbdlem  45699  infrnmptle  45866  infxrunb3rnmpt  45871  climinff  46056  xlimmnfv  46277  xlimpnfv  46281  cncfshift  46317  stoweidlem53  46496  stoweidlem57  46500  fourierdlem48  46597  fourierdlem73  46622  sge0gerp  46838  sge0resplit  46849  sge0reuz  46890  meaiuninc3v  46927  smfsup  47257  smfsupmpt  47258  smfinf  47261  smfinfmpt  47262  cbvrex2  47567  2reu8i  47576  mogoldbb  48276