Theorem nfrexw 3310

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 2401. See nfrex 3360 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 1836	. . 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 1576	1 ⊢ Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑

This proof depends on syntax axioms:  ⊤wtru 1570  Ⅎwnf 1815  Ⅎwnfc 2907  ∃wrex 3086

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-10 2177  ax-11 2193  ax-12 2212

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-nf 1816  df-clel 2835  df-nfc 2909  df-ral 3077  df-rex 3087

This theorem is used by:  nfiun  4981  rexopabb  5502  nffr  5624  abrexex2g  7980  indexfi  9357  nfoi  9515  ixpiunwdom  9591  hsmexlem2  10512  iunfo  10630  iundom2g  10631  reclem2pr  11140  nfwrd  14695  nfsum1  15866  nfsum  15867  nfcprod1  16086  nfcprod  16087  ptclsg  23943  iunmbl2  25887  mbfsup  25994  limciun  26223  opreu2reuALT  33124  iundisjf  33234  xrofsup  33409  locfinreflem  34522  esum2d  34775  bnj873  35604  bnj1014  35641  bnj1123  35666  bnj1307  35703  bnj1445  35724  bnj1446  35725  bnj1467  35734  bnj1463  35735  rmo6  35760  onvf1odlem2  35983  srepdf  36038  poimirlem24  38699  poimirlem26  38701  poimirlem27  38702  indexa  38804  filbcmb  38811  sdclem2  38813  sdclem1  38814  fdc1  38817  rexrabdioph  43938  rexfrabdioph  43939  elnn0rabdioph  43947  dvdsrabdioph  43954  oaun3lem1  44513  modelaxreplem3  46106  modelaxrep  46107  permaxrep  46132  disjrnmpt2  46339  rnmptbdlem  46403  infrnmptle  46569  infxrunb3rnmpt  46574  climinff  46759  xlimmnfv  46980  xlimpnfv  46984  cncfshift  47020  stoweidlem53  47199  stoweidlem57  47203  fourierdlem48  47300  fourierdlem73  47325  sge0gerp  47541  sge0resplit  47552  sge0reuz  47593  meaiuninc3v  47630  smfsup  47960  smfsupmpt  47961  smfinf  47964  smfinfmpt  47965  cbvrex2  48311  2reu8i  48320  mogoldbb  49019  nfrals  51111