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 2403. See nfrex 3362 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 1824	. . 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 1567	1 ⊢ Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑

Syntax hints:  ⊤wtru 1561  Ⅎwnf 1803  Ⅎwnfc 2909  ∃wrex 3086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-10 2175  ax-11 2191  ax-12 2212

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1563  df-ex 1800  df-nf 1804  df-clel 2837  df-nfc 2911  df-ral 3077  df-rex 3087

This theorem is referenced by:  nfiun  4981  rexopabb  5498  nffr  5620  abrexex2g  7945  indexfi  9303  nfoi  9462  ixpiunwdom  9538  hsmexlem2  10384  iunfo  10496  iundom2g  10497  reclem2pr  11006  nfwrd  14556  nfsum1  15717  nfsum  15718  nfcprod1  15938  nfcprod  15939  ptclsg  23675  iunmbl2  25619  mbfsup  25726  limciun  25956  opreu2reuALT  32676  iundisjf  32789  xrofsup  32969  locfinreflem  34137  esum2d  34390  bnj873  35219  bnj1014  35256  bnj1123  35281  bnj1307  35318  bnj1445  35339  bnj1446  35340  bnj1467  35349  bnj1463  35350  onvf1odlem2  35447  poimirlem24  38143  poimirlem26  38145  poimirlem27  38146  indexa  38232  filbcmb  38239  sdclem2  38241  sdclem1  38242  fdc1  38245  rexrabdioph  43371  rexfrabdioph  43372  elnn0rabdioph  43380  dvdsrabdioph  43387  oaun3lem1  43951  modelaxreplem3  45556  modelaxrep  45557  permaxrep  45582  disjrnmpt2  45766  rnmptbdlem  45830  infrnmptle  45997  infxrunb3rnmpt  46002  climinff  46187  xlimmnfv  46408  xlimpnfv  46412  cncfshift  46448  stoweidlem53  46627  stoweidlem57  46631  fourierdlem48  46728  fourierdlem73  46753  sge0gerp  46969  sge0resplit  46980  sge0reuz  47021  meaiuninc3v  47058  smfsup  47388  smfsupmpt  47389  smfinf  47392  smfinfmpt  47393  cbvrex2  47698  2reu8i  47707  mogoldbb  48407