Theorem nfrex 3312

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 2389. See nfrexg 3313 for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 20-Jan-2024.)

Hypotheses

Ref	Expression
nfrex.1	⊢ Ⅎ𝑥𝐴
nfrex.2	⊢ Ⅎ𝑥𝜑

Assertion

Ref	Expression
nfrex	⊢ Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑

Distinct variable group:   𝑥,𝑦

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐴(𝑥,𝑦)

Proof of Theorem nfrex

Step	Hyp	Ref	Expression
1		nftru 1804	. . 3 ⊢ Ⅎ𝑦⊤
2		nfrex.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3	2	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝐴)
4		nfrex.2	. . . 4 ⊢ Ⅎ𝑥𝜑
5	4	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝜑)
6	1, 3, 5	nfrexd 3310	. 2 ⊢ (⊤ → Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑)
7	6	mptru 1543	1 ⊢ Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑

Syntax hints:  ⊤wtru 1537  Ⅎwnf 1783  Ⅎwnfc 2964  ∃wrex 3142

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1539  df-ex 1780  df-nf 1784  df-cleq 2817  df-clel 2896  df-nfc 2966  df-ral 3146  df-rex 3147

This theorem is referenced by:  r19.12OLD  3330  nfiun  4952  rexopabb  5418  nffr  5532  abrexex2g  7668  indexfi  8835  nfoi  8981  ixpiunwdom  9058  hsmexlem2  9852  iunfo  9964  iundom2g  9965  reclem2pr  10473  nfwrd  13897  nfsum1  15049  nfsumw  15050  nfsum  15051  nfcprod1  15267  nfcprod  15268  ptclsg  22226  iunmbl2  24161  mbfsup  24268  limciun  24495  opreu2reuALT  30243  iundisjf  30342  xrofsup  30495  locfinreflem  31108  esum2d  31356  bnj873  32200  bnj1014  32237  bnj1123  32262  bnj1307  32299  bnj1445  32320  bnj1446  32321  bnj1467  32330  bnj1463  32331  poimirlem24  34920  poimirlem26  34922  poimirlem27  34923  indexa  35012  filbcmb  35019  sdclem2  35021  sdclem1  35022  fdc1  35025  sbcrexgOLD  39388  rexrabdioph  39397  rexfrabdioph  39398  elnn0rabdioph  39406  dvdsrabdioph  39413  disjrnmpt2  41455  rnmptbdlem  41533  infrnmptle  41703  infxrunb3rnmpt  41708  climinff  41898  xlimmnfv  42121  xlimpnfv  42125  cncfshift  42163  stoweidlem53  42345  stoweidlem57  42349  fourierdlem48  42446  fourierdlem73  42471  sge0gerp  42684  sge0resplit  42695  sge0reuz  42736  meaiuninc3v  42773  smfsup  43095  smfsupmpt  43096  smfinf  43099  smfinfmpt  43100  cbvrex2  43309  2reu8i  43319  mogoldbb  43957