Theorem nfrexw 3311

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 2372. See nfrex 3372 for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 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 1807	. . 3 ⊢ Ⅎ𝑦⊤
2		nfralw.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3	2	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝐴)
4		nfralw.2	. . . 4 ⊢ Ⅎ𝑥𝜑
5	4	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝜑)
6	1, 3, 5	nfrexdw 3308	. 2 ⊢ (⊤ → Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑)
7	6	mptru 1549	1 ⊢ Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑

Syntax hints:  ⊤wtru 1543  Ⅎwnf 1786  Ⅎwnfc 2884  ∃wrex 3071

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-10 2138  ax-11 2155  ax-12 2172

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-nf 1787  df-clel 2811  df-nfc 2886  df-ral 3063  df-rex 3072

This theorem is referenced by:  nfiun  5028  rexopabb  5529  nffr  5651  abrexex2g  7951  indexfi  9360  nfoi  9509  ixpiunwdom  9585  hsmexlem2  10422  iunfo  10534  iundom2g  10535  reclem2pr  11043  nfwrd  14493  nfsum1  15636  nfsum  15637  nfcprod1  15854  nfcprod  15855  ptclsg  23119  iunmbl2  25074  mbfsup  25181  limciun  25411  opreu2reuALT  31748  iundisjf  31851  xrofsup  32011  locfinreflem  32851  esum2d  33122  bnj873  33966  bnj1014  34003  bnj1123  34028  bnj1307  34065  bnj1445  34086  bnj1446  34087  bnj1467  34096  bnj1463  34097  poimirlem24  36560  poimirlem26  36562  poimirlem27  36563  indexa  36649  filbcmb  36656  sdclem2  36658  sdclem1  36659  fdc1  36662  sbcrexgOLD  41571  rexrabdioph  41580  rexfrabdioph  41581  elnn0rabdioph  41589  dvdsrabdioph  41596  oaun3lem1  42172  disjrnmpt2  43934  rnmptbdlem  44007  infrnmptle  44181  infxrunb3rnmpt  44186  climinff  44375  xlimmnfv  44598  xlimpnfv  44602  cncfshift  44638  stoweidlem53  44817  stoweidlem57  44821  fourierdlem48  44918  fourierdlem73  44943  sge0gerp  45159  sge0resplit  45170  sge0reuz  45211  meaiuninc3v  45248  smfsup  45578  smfsupmpt  45579  smfinf  45582  smfinfmpt  45583  cbvrex2  45860  2reu8i  45869  mogoldbb  46501