Theorem nfrexw 3284

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 2370. See nfrex 3346 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 1804	. . 3 ⊢ Ⅎ𝑦⊤
2		nfralw.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3	2	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝐴)
4		nfralw.2	. . . 4 ⊢ Ⅎ𝑥𝜑
5	4	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝜑)
6	1, 3, 5	nfrexdw 3282	. 2 ⊢ (⊤ → Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑)
7	6	mptru 1547	1 ⊢ Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑

Syntax hints:  ⊤wtru 1541  Ⅎwnf 1783  Ⅎwnfc 2876  ∃wrex 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-10 2142  ax-11 2158  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-nf 1784  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054

This theorem is referenced by:  nfiun  4983  rexopabb  5483  nffr  5604  abrexex2g  7922  indexfi  9287  nfoi  9443  ixpiunwdom  9519  hsmexlem2  10356  iunfo  10468  iundom2g  10469  reclem2pr  10977  nfwrd  14484  nfsum1  15632  nfsum  15633  nfcprod1  15850  nfcprod  15851  ptclsg  23535  iunmbl2  25491  mbfsup  25598  limciun  25828  opreu2reuALT  32456  iundisjf  32568  xrofsup  32740  locfinreflem  33823  esum2d  34076  bnj873  34907  bnj1014  34944  bnj1123  34969  bnj1307  35006  bnj1445  35027  bnj1446  35028  bnj1467  35037  bnj1463  35038  onvf1odlem2  35084  poimirlem24  37631  poimirlem26  37633  poimirlem27  37634  indexa  37720  filbcmb  37727  sdclem2  37729  sdclem1  37730  fdc1  37733  sbcrexgOLD  42766  rexrabdioph  42775  rexfrabdioph  42776  elnn0rabdioph  42784  dvdsrabdioph  42791  oaun3lem1  43356  modelaxreplem3  44963  modelaxrep  44964  permaxrep  44989  disjrnmpt2  45175  rnmptbdlem  45242  infrnmptle  45412  infxrunb3rnmpt  45417  climinff  45602  xlimmnfv  45825  xlimpnfv  45829  cncfshift  45865  stoweidlem53  46044  stoweidlem57  46048  fourierdlem48  46145  fourierdlem73  46170  sge0gerp  46386  sge0resplit  46397  sge0reuz  46438  meaiuninc3v  46475  smfsup  46805  smfsupmpt  46806  smfinf  46809  smfinfmpt  46810  cbvrex2  47098  2reu8i  47107  mogoldbb  47779