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 2370. See nfrex 3349 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 3284	. 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  4987  rexopabb  5488  nffr  5611  abrexex2g  7943  indexfi  9311  nfoi  9467  ixpiunwdom  9543  hsmexlem2  10380  iunfo  10492  iundom2g  10493  reclem2pr  11001  nfwrd  14508  nfsum1  15656  nfsum  15657  nfcprod1  15874  nfcprod  15875  ptclsg  23502  iunmbl2  25458  mbfsup  25565  limciun  25795  opreu2reuALT  32406  iundisjf  32518  xrofsup  32690  locfinreflem  33830  esum2d  34083  bnj873  34914  bnj1014  34951  bnj1123  34976  bnj1307  35013  bnj1445  35034  bnj1446  35035  bnj1467  35044  bnj1463  35045  onvf1odlem2  35091  poimirlem24  37638  poimirlem26  37640  poimirlem27  37641  indexa  37727  filbcmb  37734  sdclem2  37736  sdclem1  37737  fdc1  37740  sbcrexgOLD  42773  rexrabdioph  42782  rexfrabdioph  42783  elnn0rabdioph  42791  dvdsrabdioph  42798  oaun3lem1  43363  modelaxreplem3  44970  modelaxrep  44971  permaxrep  44996  disjrnmpt2  45182  rnmptbdlem  45249  infrnmptle  45419  infxrunb3rnmpt  45424  climinff  45609  xlimmnfv  45832  xlimpnfv  45836  cncfshift  45872  stoweidlem53  46051  stoweidlem57  46055  fourierdlem48  46152  fourierdlem73  46177  sge0gerp  46393  sge0resplit  46404  sge0reuz  46445  meaiuninc3v  46482  smfsup  46812  smfsupmpt  46813  smfinf  46816  smfinfmpt  46817  cbvrex2  47105  2reu8i  47114  mogoldbb  47786