Theorem nfrex 3237

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 nfrexg 3238 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 1808	. . 3 ⊢ Ⅎ𝑦⊤
2		nfrex.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3	2	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝐴)
4		nfrex.2	. . . 4 ⊢ Ⅎ𝑥𝜑
5	4	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝜑)
6	1, 3, 5	nfrexd 3235	. 2 ⊢ (⊤ → Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑)
7	6	mptru 1546	1 ⊢ Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑

Syntax hints:  ⊤wtru 1540  Ⅎwnf 1787  Ⅎwnfc 2886  ∃wrex 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-10 2139  ax-11 2156  ax-12 2173

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-nf 1788  df-clel 2817  df-nfc 2888  df-ral 3068  df-rex 3069

This theorem is referenced by:  nfiun  4951  rexopabb  5434  nffr  5554  abrexex2g  7780  indexfi  9057  nfoi  9203  ixpiunwdom  9279  hsmexlem2  10114  iunfo  10226  iundom2g  10227  reclem2pr  10735  nfwrd  14174  nfsum1  15329  nfsum  15330  nfsumOLD  15331  nfcprod1  15548  nfcprod  15549  ptclsg  22674  iunmbl2  24626  mbfsup  24733  limciun  24963  opreu2reuALT  30726  iundisjf  30829  xrofsup  30992  locfinreflem  31692  esum2d  31961  bnj873  32804  bnj1014  32841  bnj1123  32866  bnj1307  32903  bnj1445  32924  bnj1446  32925  bnj1467  32934  bnj1463  32935  poimirlem24  35728  poimirlem26  35730  poimirlem27  35731  indexa  35818  filbcmb  35825  sdclem2  35827  sdclem1  35828  fdc1  35831  sbcrexgOLD  40523  rexrabdioph  40532  rexfrabdioph  40533  elnn0rabdioph  40541  dvdsrabdioph  40548  disjrnmpt2  42615  rnmptbdlem  42690  infrnmptle  42853  infxrunb3rnmpt  42858  climinff  43042  xlimmnfv  43265  xlimpnfv  43269  cncfshift  43305  stoweidlem53  43484  stoweidlem57  43488  fourierdlem48  43585  fourierdlem73  43610  sge0gerp  43823  sge0resplit  43834  sge0reuz  43875  meaiuninc3v  43912  smfsup  44234  smfsupmpt  44235  smfinf  44238  smfinfmpt  44239  cbvrex2  44483  2reu8i  44492  mogoldbb  45125