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

Theorem nfrex 3155
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 1878 . . 3 𝑦
2 nfrex.1 . . . 4 𝑥𝐴
32a1i 11 . . 3 (⊤ → 𝑥𝐴)
4 nfrex.2 . . . 4 𝑥𝜑
54a1i 11 . . 3 (⊤ → Ⅎ𝑥𝜑)
61, 3, 5nfrexd 3154 . 2 (⊤ → Ⅎ𝑥𝑦𝐴 𝜑)
76trud 1641 1 𝑥𝑦𝐴 𝜑
Colors of variables: wff setvar class
Syntax hints:  wtru 1632  wnf 1856  wnfc 2900  wrex 3062
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-tru 1634  df-ex 1853  df-nf 1858  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-rex 3067
This theorem is referenced by:  r19.12  3211  nfuni  4580  nfiun  4682  nffr  5223  abrexex2g  7291  abrexex2OLD  7297  indexfi  8430  nfoi  8575  ixpiunwdom  8652  hsmexlem2  9451  iunfo  9563  iundom2g  9564  reclem2pr  10072  nfwrd  13529  nfsum1  14628  nfsum  14629  nfcprod1  14847  nfcprod  14848  ptclsg  21639  iunmbl2  23545  mbfsup  23651  limciun  23878  iundisjf  29740  xrofsup  29873  locfinreflem  30247  esum2d  30495  bnj873  31332  bnj1014  31368  bnj1123  31392  bnj1307  31429  bnj1445  31450  bnj1446  31451  bnj1467  31460  bnj1463  31461  cnfinltrel  33578  poimirlem24  33766  poimirlem26  33768  poimirlem27  33769  indexa  33860  filbcmb  33867  sdclem2  33870  sdclem1  33871  fdc1  33874  sbcrexgOLD  37875  rexrabdioph  37884  rexfrabdioph  37885  elnn0rabdioph  37893  dvdsrabdioph  37900  disjrnmpt2  39895  rnmptbdlem  39988  infrnmptle  40166  infxrunb3rnmpt  40171  climinff  40361  xlimmnfv  40578  xlimpnfv  40582  cncfshift  40605  stoweidlem53  40787  stoweidlem57  40791  fourierdlem48  40888  fourierdlem73  40913  sge0gerp  41129  sge0resplit  41140  sge0reuz  41181  meaiuninc3v  41218  smfsup  41540  smfsupmpt  41541  smfinf  41544  smfinfmpt  41545  cbvrex2  41693  mogoldbb  42201
  Copyright terms: Public domain W3C validator