Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfrex Structured version   Visualization version   GIF version

Theorem nfrex 2990
 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
StepHypRef Expression
1 nftru 1721 . . 3 𝑦
2 nfrex.1 . . . 4 𝑥𝐴
32a1i 11 . . 3 (⊤ → 𝑥𝐴)
4 nfrex.2 . . . 4 𝑥𝜑
54a1i 11 . . 3 (⊤ → Ⅎ𝑥𝜑)
61, 3, 5nfrexd 2989 . 2 (⊤ → Ⅎ𝑥𝑦𝐴 𝜑)
76trud 1484 1 𝑥𝑦𝐴 𝜑
 Colors of variables: wff setvar class Syntax hints:  ⊤wtru 1476  Ⅎwnf 1699  Ⅎwnfc 2738  ∃wrex 2897 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902 This theorem is referenced by:  r19.12  3045  nfuni  4378  rabasiun  4459  nfiun  4484  nffr  5012  abrexex2g  7036  abrexex2  7040  indexfi  8157  nfoi  8302  ixpiunwdom  8379  hsmexlem2  9132  iunfo  9240  iundom2g  9241  reclem2pr  9749  nfwrd  13188  nfsum1  14268  nfsum  14269  nfcprod1  14479  nfcprod  14480  ptclsg  21228  iunmbl2  23132  mbfsup  23237  limciun  23464  iundisjf  28784  xrofsup  28923  locfinreflem  29235  esum2d  29482  bnj873  30248  bnj1014  30284  bnj1123  30308  bnj1307  30345  bnj1445  30366  bnj1446  30367  bnj1467  30376  bnj1463  30377  poimirlem24  32603  poimirlem26  32605  poimirlem27  32606  indexa  32698  filbcmb  32705  sdclem2  32708  sdclem1  32709  fdc1  32712  sbcrexgOLD  36367  rexrabdioph  36376  rexfrabdioph  36377  elnn0rabdioph  36385  dvdsrabdioph  36392  disjrnmpt2  38370  climinff  38678  cncfshift  38759  stoweidlem53  38946  stoweidlem57  38950  fourierdlem48  39047  fourierdlem73  39072  sge0gerp  39288  sge0resplit  39299  sge0reuz  39340  cbvrex2  39822
 Copyright terms: Public domain W3C validator