Theorem nfrex 3307

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 2384. See nfrexg 3308 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 1799	. . 3 ⊢ Ⅎ𝑦⊤
2		nfrex.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3	2	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝐴)
4		nfrex.2	. . . 4 ⊢ Ⅎ𝑥𝜑
5	4	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝜑)
6	1, 3, 5	nfrexd 3305	. 2 ⊢ (⊤ → Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑)
7	6	mptru 1538	1 ⊢ Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑

Syntax hints:  ⊤wtru 1532  Ⅎwnf 1778  Ⅎwnfc 2959  ∃wrex 3137

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1534  df-ex 1775  df-nf 1779  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ral 3141  df-rex 3142

This theorem is referenced by:  r19.12OLD  3325  nfiun  4940  rexopabb  5406  nffr  5522  abrexex2g  7657  indexfi  8824  nfoi  8970  ixpiunwdom  9047  hsmexlem2  9841  iunfo  9953  iundom2g  9954  reclem2pr  10462  nfwrd  13886  nfsum1  15038  nfsumw  15039  nfsum  15040  nfcprod1  15256  nfcprod  15257  ptclsg  22215  iunmbl2  24150  mbfsup  24257  limciun  24484  opreu2reuALT  30232  iundisjf  30331  xrofsup  30484  locfinreflem  31097  esum2d  31345  bnj873  32189  bnj1014  32226  bnj1123  32251  bnj1307  32288  bnj1445  32309  bnj1446  32310  bnj1467  32319  bnj1463  32320  poimirlem24  34908  poimirlem26  34910  poimirlem27  34911  indexa  35000  filbcmb  35007  sdclem2  35009  sdclem1  35010  fdc1  35013  sbcrexgOLD  39372  rexrabdioph  39381  rexfrabdioph  39382  elnn0rabdioph  39390  dvdsrabdioph  39397  disjrnmpt2  41438  rnmptbdlem  41516  infrnmptle  41686  infxrunb3rnmpt  41691  climinff  41881  xlimmnfv  42104  xlimpnfv  42108  cncfshift  42146  stoweidlem53  42328  stoweidlem57  42332  fourierdlem48  42429  fourierdlem73  42454  sge0gerp  42667  sge0resplit  42678  sge0reuz  42719  meaiuninc3v  42756  smfsup  43078  smfsupmpt  43079  smfinf  43082  smfinfmpt  43083  cbvrex2  43292  2reu8i  43302  mogoldbb  43940