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

Theorem nfrex 3001
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 1727 . . 3 𝑦
2 nfrex.1 . . . 4 𝑥𝐴
32a1i 11 . . 3 (⊤ → 𝑥𝐴)
4 nfrex.2 . . . 4 𝑥𝜑
54a1i 11 . . 3 (⊤ → Ⅎ𝑥𝜑)
61, 3, 5nfrexd 3000 . 2 (⊤ → Ⅎ𝑥𝑦𝐴 𝜑)
76trud 1490 1 𝑥𝑦𝐴 𝜑
Colors of variables: wff setvar class
Syntax hints:  wtru 1481  wnf 1705  wnfc 2748  wrex 2908
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-rex 2913
This theorem is referenced by:  r19.12  3056  nfuni  4408  rabasiun  4489  nfiun  4514  nffr  5048  abrexex2g  7090  abrexex2  7094  indexfi  8218  nfoi  8363  ixpiunwdom  8440  hsmexlem2  9193  iunfo  9305  iundom2g  9306  reclem2pr  9814  nfwrd  13272  nfsum1  14354  nfsum  14355  nfcprod1  14565  nfcprod  14566  ptclsg  21328  iunmbl2  23232  mbfsup  23337  limciun  23564  iundisjf  29244  xrofsup  29374  locfinreflem  29686  esum2d  29933  bnj873  30699  bnj1014  30735  bnj1123  30759  bnj1307  30796  bnj1445  30817  bnj1446  30818  bnj1467  30827  bnj1463  30828  poimirlem24  33062  poimirlem26  33064  poimirlem27  33065  indexa  33157  filbcmb  33164  sdclem2  33167  sdclem1  33168  fdc1  33171  sbcrexgOLD  36826  rexrabdioph  36835  rexfrabdioph  36836  elnn0rabdioph  36844  dvdsrabdioph  36851  disjrnmpt2  38846  rnmptbdlem  38943  infrnmptle  39111  infxrunb3rnmpt  39116  climinff  39244  cncfshift  39387  stoweidlem53  39574  stoweidlem57  39578  fourierdlem48  39675  fourierdlem73  39700  sge0gerp  39916  sge0resplit  39927  sge0reuz  39968  smfsup  40324  smfsupmpt  40325  smfinf  40328  smfinfmpt  40329  cbvrex2  40474
  Copyright terms: Public domain W3C validator