Theorem nfrexw 3280

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 2372. See nfrex 3341 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 1805	. . 3 ⊢ Ⅎ𝑦⊤
2		nfralw.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3	2	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝐴)
4		nfralw.2	. . . 4 ⊢ Ⅎ𝑥𝜑
5	4	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝜑)
6	1, 3, 5	nfrexdw 3278	. 2 ⊢ (⊤ → Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑)
7	6	mptru 1548	1 ⊢ Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑

Syntax hints:  ⊤wtru 1542  Ⅎwnf 1784  Ⅎwnfc 2879  ∃wrex 3056

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-10 2144  ax-11 2160  ax-12 2180

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-nf 1785  df-clel 2806  df-nfc 2881  df-ral 3048  df-rex 3057

This theorem is referenced by:  nfiun  4971  rexopabb  5466  nffr  5587  abrexex2g  7896  indexfi  9244  nfoi  9400  ixpiunwdom  9476  hsmexlem2  10318  iunfo  10430  iundom2g  10431  reclem2pr  10939  nfwrd  14450  nfsum1  15597  nfsum  15598  nfcprod1  15815  nfcprod  15816  ptclsg  23530  iunmbl2  25485  mbfsup  25592  limciun  25822  opreu2reuALT  32456  iundisjf  32569  xrofsup  32750  locfinreflem  33853  esum2d  34106  bnj873  34936  bnj1014  34973  bnj1123  34998  bnj1307  35035  bnj1445  35056  bnj1446  35057  bnj1467  35066  bnj1463  35067  onvf1odlem2  35148  poimirlem24  37694  poimirlem26  37696  poimirlem27  37697  indexa  37783  filbcmb  37790  sdclem2  37792  sdclem1  37793  fdc1  37796  sbcrexgOLD  42888  rexrabdioph  42897  rexfrabdioph  42898  elnn0rabdioph  42906  dvdsrabdioph  42913  oaun3lem1  43477  modelaxreplem3  45083  modelaxrep  45084  permaxrep  45109  disjrnmpt2  45295  rnmptbdlem  45362  infrnmptle  45531  infxrunb3rnmpt  45536  climinff  45721  xlimmnfv  45942  xlimpnfv  45946  cncfshift  45982  stoweidlem53  46161  stoweidlem57  46165  fourierdlem48  46262  fourierdlem73  46287  sge0gerp  46503  sge0resplit  46514  sge0reuz  46555  meaiuninc3v  46592  smfsup  46922  smfsupmpt  46923  smfinf  46926  smfinfmpt  46927  cbvrex2  47214  2reu8i  47223  mogoldbb  47895