Theorem nfrex 3243

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

Syntax hints:  ⊤wtru 1540  Ⅎwnf 1786  Ⅎwnfc 2888  ∃wrex 3066

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-10 2138  ax-11 2155  ax-12 2172

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-nf 1787  df-clel 2817  df-nfc 2890  df-ral 3070  df-rex 3071

This theorem is referenced by:  nfiun  4955  rexopabb  5442  nffr  5564  abrexex2g  7816  indexfi  9136  nfoi  9282  ixpiunwdom  9358  hsmexlem2  10192  iunfo  10304  iundom2g  10305  reclem2pr  10813  nfwrd  14255  nfsum1  15410  nfsum  15411  nfsumOLD  15412  nfcprod1  15629  nfcprod  15630  ptclsg  22775  iunmbl2  24730  mbfsup  24837  limciun  25067  opreu2reuALT  30834  iundisjf  30937  xrofsup  31099  locfinreflem  31799  esum2d  32070  bnj873  32913  bnj1014  32950  bnj1123  32975  bnj1307  33012  bnj1445  33033  bnj1446  33034  bnj1467  33043  bnj1463  33044  poimirlem24  35810  poimirlem26  35812  poimirlem27  35813  indexa  35900  filbcmb  35907  sdclem2  35909  sdclem1  35910  fdc1  35913  sbcrexgOLD  40614  rexrabdioph  40623  rexfrabdioph  40624  elnn0rabdioph  40632  dvdsrabdioph  40639  disjrnmpt2  42733  rnmptbdlem  42808  infrnmptle  42970  infxrunb3rnmpt  42975  climinff  43159  xlimmnfv  43382  xlimpnfv  43386  cncfshift  43422  stoweidlem53  43601  stoweidlem57  43605  fourierdlem48  43702  fourierdlem73  43727  sge0gerp  43940  sge0resplit  43951  sge0reuz  43992  meaiuninc3v  44029  smfsup  44358  smfsupmpt  44359  smfinf  44362  smfinfmpt  44363  cbvrex2  44607  2reu8i  44616  mogoldbb  45248