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

Theorem nfrexw 3310
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 2371. See nfrex 3371 for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 20-Jan-2024.)
Hypotheses
Ref Expression
nfralw.1 𝑥𝐴
nfralw.2 𝑥𝜑
Assertion
Ref Expression
nfrexw 𝑥𝑦𝐴 𝜑
Distinct variable group:   𝑥,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐴(𝑥,𝑦)

Proof of Theorem nfrexw
StepHypRef Expression
1 nftru 1806 . . 3 𝑦
2 nfralw.1 . . . 4 𝑥𝐴
32a1i 11 . . 3 (⊤ → 𝑥𝐴)
4 nfralw.2 . . . 4 𝑥𝜑
54a1i 11 . . 3 (⊤ → Ⅎ𝑥𝜑)
61, 3, 5nfrexdw 3307 . 2 (⊤ → Ⅎ𝑥𝑦𝐴 𝜑)
76mptru 1548 1 𝑥𝑦𝐴 𝜑
Colors of variables: wff setvar class
Syntax hints:  wtru 1542  wnf 1785  wnfc 2883  wrex 3070
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-10 2137  ax-11 2154  ax-12 2171
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-nf 1786  df-clel 2810  df-nfc 2885  df-ral 3062  df-rex 3071
This theorem is referenced by:  nfiun  5021  rexopabb  5522  nffr  5644  abrexex2g  7935  indexfi  9345  nfoi  9493  ixpiunwdom  9569  hsmexlem2  10406  iunfo  10518  iundom2g  10519  reclem2pr  11027  nfwrd  14477  nfsum1  15620  nfsum  15621  nfcprod1  15838  nfcprod  15839  ptclsg  23050  iunmbl2  25005  mbfsup  25112  limciun  25342  opreu2reuALT  31644  iundisjf  31749  xrofsup  31915  locfinreflem  32715  esum2d  32986  bnj873  33830  bnj1014  33867  bnj1123  33892  bnj1307  33929  bnj1445  33950  bnj1446  33951  bnj1467  33960  bnj1463  33961  poimirlem24  36380  poimirlem26  36382  poimirlem27  36383  indexa  36470  filbcmb  36477  sdclem2  36479  sdclem1  36480  fdc1  36483  sbcrexgOLD  41358  rexrabdioph  41367  rexfrabdioph  41368  elnn0rabdioph  41376  dvdsrabdioph  41383  oaun3lem1  41959  disjrnmpt2  43721  rnmptbdlem  43796  infrnmptle  43970  infxrunb3rnmpt  43975  climinff  44164  xlimmnfv  44387  xlimpnfv  44391  cncfshift  44427  stoweidlem53  44606  stoweidlem57  44610  fourierdlem48  44707  fourierdlem73  44732  sge0gerp  44948  sge0resplit  44959  sge0reuz  45000  meaiuninc3v  45037  smfsup  45367  smfsupmpt  45368  smfinf  45371  smfinfmpt  45372  cbvrex2  45648  2reu8i  45657  mogoldbb  46289
  Copyright terms: Public domain W3C validator