Theorem nfrex 3188

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.)

Hypotheses

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

Assertion

Ref	Expression
nfrex	⊢ Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑

Proof of Theorem nfrex

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

Syntax hints:  ⊤wtru 1602  Ⅎwnf 1827  Ⅎwnfc 2919  ∃wrex 3091

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ral 3095  df-rex 3096

This theorem is referenced by:  r19.12  3248  r19.12OLD  3249  nfuni  4677  nfiun  4781  nffr  5329  abrexex2g  7422  indexfi  8562  nfoi  8708  ixpiunwdom  8785  hsmexlem2  9584  iunfo  9696  iundom2g  9697  reclem2pr  10205  nfwrd  13632  nfsum1  14828  nfsum  14829  nfcprod1  15043  nfcprod  15044  ptclsg  21827  iunmbl2  23761  mbfsup  23868  limciun  24095  iundisjf  29965  xrofsup  30098  locfinreflem  30505  esum2d  30753  bnj873  31593  bnj1014  31629  bnj1123  31653  bnj1307  31690  bnj1445  31711  bnj1446  31712  bnj1467  31721  bnj1463  31722  cnfinltrel  33836  poimirlem24  34059  poimirlem26  34061  poimirlem27  34062  indexa  34153  filbcmb  34160  sdclem2  34162  sdclem1  34163  fdc1  34166  sbcrexgOLD  38309  rexrabdioph  38318  rexfrabdioph  38319  elnn0rabdioph  38327  dvdsrabdioph  38334  disjrnmpt2  40298  rnmptbdlem  40381  infrnmptle  40556  infxrunb3rnmpt  40561  climinff  40751  xlimmnfv  40974  xlimpnfv  40978  cncfshift  41015  stoweidlem53  41197  stoweidlem57  41201  fourierdlem48  41298  fourierdlem73  41323  sge0gerp  41536  sge0resplit  41547  sge0reuz  41588  meaiuninc3v  41625  smfsup  41947  smfsupmpt  41948  smfinf  41951  smfinfmpt  41952  cbvrex2  42132  2reu8i  42154  mogoldbb  42698