Theorem nfrexw 3313

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 3375 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 3310	. 2 ⊢ (⊤ → Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑)
7	6	mptru 1547	1 ⊢ Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑

Syntax hints:  ⊤wtru 1541  Ⅎwnf 1783  Ⅎwnfc 2890  ∃wrex 3070

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 2007  ax-8 2110  ax-10 2141  ax-11 2157  ax-12 2177

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-nf 1784  df-clel 2816  df-nfc 2892  df-ral 3062  df-rex 3071

This theorem is referenced by:  nfiun  5023  rexopabb  5533  nffr  5658  abrexex2g  7989  indexfi  9400  nfoi  9554  ixpiunwdom  9630  hsmexlem2  10467  iunfo  10579  iundom2g  10580  reclem2pr  11088  nfwrd  14581  nfsum1  15726  nfsum  15727  nfcprod1  15944  nfcprod  15945  ptclsg  23623  iunmbl2  25592  mbfsup  25699  limciun  25929  opreu2reuALT  32496  iundisjf  32602  xrofsup  32771  locfinreflem  33839  esum2d  34094  bnj873  34938  bnj1014  34975  bnj1123  35000  bnj1307  35037  bnj1445  35058  bnj1446  35059  bnj1467  35068  bnj1463  35069  poimirlem24  37651  poimirlem26  37653  poimirlem27  37654  indexa  37740  filbcmb  37747  sdclem2  37749  sdclem1  37750  fdc1  37753  sbcrexgOLD  42796  rexrabdioph  42805  rexfrabdioph  42806  elnn0rabdioph  42814  dvdsrabdioph  42821  oaun3lem1  43387  modelaxreplem3  44997  modelaxrep  44998  disjrnmpt2  45193  rnmptbdlem  45262  infrnmptle  45434  infxrunb3rnmpt  45439  climinff  45626  xlimmnfv  45849  xlimpnfv  45853  cncfshift  45889  stoweidlem53  46068  stoweidlem57  46072  fourierdlem48  46169  fourierdlem73  46194  sge0gerp  46410  sge0resplit  46421  sge0reuz  46462  meaiuninc3v  46499  smfsup  46829  smfsupmpt  46830  smfinf  46833  smfinfmpt  46834  cbvrex2  47116  2reu8i  47125  mogoldbb  47772