Theorem nfrexw 3285

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 2376. See nfrex 3337 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 3283	. 2 ⊢ (⊤ → Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑)
7	6	mptru 1549	1 ⊢ Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑

Syntax hints:  ⊤wtru 1543  Ⅎwnf 1785  Ⅎwnfc 2883  ∃wrex 3061

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 2811  df-nfc 2885  df-ral 3052  df-rex 3062

This theorem is referenced by:  nfiun  4965  rexopabb  5483  nffr  5604  abrexex2g  7917  indexfi  9270  nfoi  9429  ixpiunwdom  9505  hsmexlem2  10349  iunfo  10461  iundom2g  10462  reclem2pr  10971  nfwrd  14505  nfsum1  15652  nfsum  15653  nfcprod1  15873  nfcprod  15874  ptclsg  23580  iunmbl2  25524  mbfsup  25631  limciun  25861  opreu2reuALT  32546  iundisjf  32659  xrofsup  32840  locfinreflem  33984  esum2d  34237  bnj873  35066  bnj1014  35103  bnj1123  35128  bnj1307  35165  bnj1445  35186  bnj1446  35187  bnj1467  35196  bnj1463  35197  onvf1odlem2  35286  poimirlem24  37965  poimirlem26  37967  poimirlem27  37968  indexa  38054  filbcmb  38061  sdclem2  38063  sdclem1  38064  fdc1  38067  rexrabdioph  43222  rexfrabdioph  43223  elnn0rabdioph  43231  dvdsrabdioph  43238  oaun3lem1  43802  modelaxreplem3  45407  modelaxrep  45408  permaxrep  45433  disjrnmpt2  45618  rnmptbdlem  45684  infrnmptle  45851  infxrunb3rnmpt  45856  climinff  46041  xlimmnfv  46262  xlimpnfv  46266  cncfshift  46302  stoweidlem53  46481  stoweidlem57  46485  fourierdlem48  46582  fourierdlem73  46607  sge0gerp  46823  sge0resplit  46834  sge0reuz  46875  meaiuninc3v  46912  smfsup  47242  smfsupmpt  47243  smfinf  47246  smfinfmpt  47247  cbvrex2  47552  2reu8i  47561  mogoldbb  48261