Theorem nfrexw 3286

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 3338 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 1806	. . 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 1549	1 ⊢ Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑

Syntax hints:  ⊤wtru 1543  Ⅎwnf 1785  Ⅎwnfc 2884  ∃wrex 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-10 2147  ax-11 2163  ax-12 2185

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-nf 1786  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063

This theorem is referenced by:  nfiun  4966  rexopabb  5476  nffr  5597  abrexex2g  7910  indexfi  9263  nfoi  9422  ixpiunwdom  9498  hsmexlem2  10340  iunfo  10452  iundom2g  10453  reclem2pr  10962  nfwrd  14496  nfsum1  15643  nfsum  15644  nfcprod1  15864  nfcprod  15865  ptclsg  23590  iunmbl2  25534  mbfsup  25641  limciun  25871  opreu2reuALT  32561  iundisjf  32674  xrofsup  32855  locfinreflem  34000  esum2d  34253  bnj873  35082  bnj1014  35119  bnj1123  35144  bnj1307  35181  bnj1445  35202  bnj1446  35203  bnj1467  35212  bnj1463  35213  onvf1odlem2  35302  poimirlem24  37979  poimirlem26  37981  poimirlem27  37982  indexa  38068  filbcmb  38075  sdclem2  38077  sdclem1  38078  fdc1  38081  sbcrexgOLD  43231  rexrabdioph  43240  rexfrabdioph  43241  elnn0rabdioph  43249  dvdsrabdioph  43256  oaun3lem1  43820  modelaxreplem3  45425  modelaxrep  45426  permaxrep  45451  disjrnmpt2  45636  rnmptbdlem  45702  infrnmptle  45869  infxrunb3rnmpt  45874  climinff  46059  xlimmnfv  46280  xlimpnfv  46284  cncfshift  46320  stoweidlem53  46499  stoweidlem57  46503  fourierdlem48  46600  fourierdlem73  46625  sge0gerp  46841  sge0resplit  46852  sge0reuz  46893  meaiuninc3v  46930  smfsup  47260  smfsupmpt  47261  smfinf  47264  smfinfmpt  47265  cbvrex2  47564  2reu8i  47573  mogoldbb  48273