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

Theorem nfrex 3268
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.) Add disjoint variable condition to avoid ax-13 2379. See nfrexg 3269 for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 20-Jan-2024.)
Hypotheses
Ref Expression
nfrex.1 𝑥𝐴
nfrex.2 𝑥𝜑
Assertion
Ref Expression
nfrex 𝑥𝑦𝐴 𝜑
Distinct variable group:   𝑥,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐴(𝑥,𝑦)

Proof of Theorem nfrex
StepHypRef Expression
1 nftru 1806 . . 3 𝑦
2 nfrex.1 . . . 4 𝑥𝐴
32a1i 11 . . 3 (⊤ → 𝑥𝐴)
4 nfrex.2 . . . 4 𝑥𝜑
54a1i 11 . . 3 (⊤ → Ⅎ𝑥𝜑)
61, 3, 5nfrexd 3266 . 2 (⊤ → Ⅎ𝑥𝑦𝐴 𝜑)
76mptru 1545 1 𝑥𝑦𝐴 𝜑
Colors of variables: wff setvar class
Syntax hints:  wtru 1539  wnf 1785  wnfc 2936  wrex 3107
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112
This theorem is referenced by:  nfiun  4911  rexopabb  5380  nffr  5493  abrexex2g  7647  indexfi  8816  nfoi  8962  ixpiunwdom  9038  hsmexlem2  9838  iunfo  9950  iundom2g  9951  reclem2pr  10459  nfwrd  13886  nfsum1  15038  nfsum  15039  nfsumOLD  15040  nfcprod1  15256  nfcprod  15257  ptclsg  22220  iunmbl2  24161  mbfsup  24268  limciun  24497  opreu2reuALT  30247  iundisjf  30352  xrofsup  30518  locfinreflem  31193  esum2d  31462  bnj873  32306  bnj1014  32343  bnj1123  32368  bnj1307  32405  bnj1445  32426  bnj1446  32427  bnj1467  32436  bnj1463  32437  poimirlem24  35081  poimirlem26  35083  poimirlem27  35084  indexa  35171  filbcmb  35178  sdclem2  35180  sdclem1  35181  fdc1  35184  sbcrexgOLD  39724  rexrabdioph  39733  rexfrabdioph  39734  elnn0rabdioph  39742  dvdsrabdioph  39749  disjrnmpt2  41813  rnmptbdlem  41891  infrnmptle  42058  infxrunb3rnmpt  42063  climinff  42251  xlimmnfv  42474  xlimpnfv  42478  cncfshift  42514  stoweidlem53  42693  stoweidlem57  42697  fourierdlem48  42794  fourierdlem73  42819  sge0gerp  43032  sge0resplit  43043  sge0reuz  43084  meaiuninc3v  43121  smfsup  43443  smfsupmpt  43444  smfinf  43447  smfinfmpt  43448  cbvrex2  43657  2reu8i  43667  mogoldbb  44301
  Copyright terms: Public domain W3C validator