Theorem nfrex 3218

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 2371. See nfrexg 3219 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 1812	. . 3 ⊢ Ⅎ𝑦⊤
2		nfrex.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3	2	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝐴)
4		nfrex.2	. . . 4 ⊢ Ⅎ𝑥𝜑
5	4	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝜑)
6	1, 3, 5	nfrexd 3216	. 2 ⊢ (⊤ → Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑)
7	6	mptru 1550	1 ⊢ Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑

Syntax hints:  ⊤wtru 1544  Ⅎwnf 1791  Ⅎwnfc 2877  ∃wrex 3052

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-10 2143  ax-11 2160  ax-12 2177

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-ex 1788  df-nf 1792  df-clel 2809  df-nfc 2879  df-ral 3056  df-rex 3057

This theorem is referenced by:  nfiun  4920  rexopabb  5394  nffr  5510  abrexex2g  7715  indexfi  8962  nfoi  9108  ixpiunwdom  9184  hsmexlem2  10006  iunfo  10118  iundom2g  10119  reclem2pr  10627  nfwrd  14063  nfsum1  15218  nfsum  15219  nfsumOLD  15220  nfcprod1  15435  nfcprod  15436  ptclsg  22466  iunmbl2  24408  mbfsup  24515  limciun  24745  opreu2reuALT  30498  iundisjf  30601  xrofsup  30764  locfinreflem  31458  esum2d  31727  bnj873  32571  bnj1014  32608  bnj1123  32633  bnj1307  32670  bnj1445  32691  bnj1446  32692  bnj1467  32701  bnj1463  32702  poimirlem24  35487  poimirlem26  35489  poimirlem27  35490  indexa  35577  filbcmb  35584  sdclem2  35586  sdclem1  35587  fdc1  35590  sbcrexgOLD  40251  rexrabdioph  40260  rexfrabdioph  40261  elnn0rabdioph  40269  dvdsrabdioph  40276  disjrnmpt2  42340  rnmptbdlem  42414  infrnmptle  42577  infxrunb3rnmpt  42582  climinff  42770  xlimmnfv  42993  xlimpnfv  42997  cncfshift  43033  stoweidlem53  43212  stoweidlem57  43216  fourierdlem48  43313  fourierdlem73  43338  sge0gerp  43551  sge0resplit  43562  sge0reuz  43603  meaiuninc3v  43640  smfsup  43962  smfsupmpt  43963  smfinf  43966  smfinfmpt  43967  cbvrex2  44211  2reu8i  44220  mogoldbb  44853