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 2402. See nfrex 3361 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 1837	. . 3 ⊢ Ⅎ𝑦⊤
2		nfralw.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3	2	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝐴)
4		nfralw.2	. . . 4 ⊢ Ⅎ𝑥𝜑
5	4	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝜑)
6	1, 3, 5	nfrexdw 3309	. 2 ⊢ (⊤ → Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑)
7	6	mptru 1577	1 ⊢ Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑

This proof depends on syntax axioms:  ⊤wtru 1571  Ⅎwnf 1816  Ⅎwnfc 2908  ∃wrex 3087

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-10 2178  ax-11 2194  ax-12 2213

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-nf 1817  df-clel 2836  df-nfc 2910  df-ral 3078  df-rex 3088

This theorem is used by:  nfiun  4982  rexopabb  5502  nffr  5624  abrexex2g  7976  indexfi  9349  nfoi  9508  ixpiunwdom  9584  hsmexlem2  10505  iunfo  10623  iundom2g  10624  reclem2pr  11133  nfwrd  14688  nfsum1  15857  nfsum  15858  nfcprod1  16077  nfcprod  16078  ptclsg  23934  iunmbl2  25878  mbfsup  25985  limciun  26214  opreu2reuALT  33073  iundisjf  33183  xrofsup  33359  locfinreflem  34472  esum2d  34725  bnj873  35554  bnj1014  35591  bnj1123  35616  bnj1307  35653  bnj1445  35674  bnj1446  35675  bnj1467  35684  bnj1463  35685  onvf1odlem2  35883  poimirlem24  38562  poimirlem26  38564  poimirlem27  38565  indexa  38667  filbcmb  38674  sdclem2  38676  sdclem1  38677  fdc1  38680  rexrabdioph  43800  rexfrabdioph  43801  elnn0rabdioph  43809  dvdsrabdioph  43816  oaun3lem1  44375  modelaxreplem3  45969  modelaxrep  45970  permaxrep  45995  disjrnmpt2  46202  rnmptbdlem  46266  infrnmptle  46432  infxrunb3rnmpt  46437  climinff  46622  xlimmnfv  46843  xlimpnfv  46847  cncfshift  46883  stoweidlem53  47062  stoweidlem57  47066  fourierdlem48  47163  fourierdlem73  47188  sge0gerp  47404  sge0resplit  47415  sge0reuz  47456  meaiuninc3v  47493  smfsup  47823  smfsupmpt  47824  smfinf  47827  smfinfmpt  47828  cbvrex2  48173  2reu8i  48182  mogoldbb  48882  nfrals  50899