Theorem nfrex 3036

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 1770	. . 3 ⊢ Ⅎ𝑦⊤
2		nfrex.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3	2	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝐴)
4		nfrex.2	. . . 4 ⊢ Ⅎ𝑥𝜑
5	4	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝜑)
6	1, 3, 5	nfrexd 3035	. 2 ⊢ (⊤ → Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑)
7	6	trud 1533	1 ⊢ Ⅎ𝑥∃𝑦 ∈ 𝐴 𝜑

Syntax hints:  ⊤wtru 1524  Ⅎwnf 1748  Ⅎwnfc 2780  ∃wrex 2942

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947

This theorem is referenced by:  r19.12  3092  nfuni  4474  nfiun  4580  nffr  5117  abrexex2g  7186  abrexex2OLD  7192  indexfi  8315  nfoi  8460  ixpiunwdom  8537  hsmexlem2  9287  iunfo  9399  iundom2g  9400  reclem2pr  9908  nfwrd  13365  nfsum1  14464  nfsum  14465  nfcprod1  14684  nfcprod  14685  ptclsg  21466  iunmbl2  23371  mbfsup  23476  limciun  23703  iundisjf  29528  xrofsup  29661  locfinreflem  30035  esum2d  30283  bnj873  31120  bnj1014  31156  bnj1123  31180  bnj1307  31217  bnj1445  31238  bnj1446  31239  bnj1467  31248  bnj1463  31249  poimirlem24  33563  poimirlem26  33565  poimirlem27  33566  indexa  33658  filbcmb  33665  sdclem2  33668  sdclem1  33669  fdc1  33672  sbcrexgOLD  37666  rexrabdioph  37675  rexfrabdioph  37676  elnn0rabdioph  37684  dvdsrabdioph  37691  disjrnmpt2  39689  rnmptbdlem  39784  infrnmptle  39963  infxrunb3rnmpt  39968  climinff  40161  xlimmnfv  40378  xlimpnfv  40382  cncfshift  40405  stoweidlem53  40588  stoweidlem57  40592  fourierdlem48  40689  fourierdlem73  40714  sge0gerp  40930  sge0resplit  40941  sge0reuz  40982  meaiuninc3v  41019  smfsup  41341  smfsupmpt  41342  smfinf  41345  smfinfmpt  41346  cbvrex2  41494  mogoldbb  41998