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

Theorem nfral 3226
Description: Bound-variable hypothesis builder for restricted quantification. (Contributed by NM, 1-Sep-1999.) (Revised by Mario Carneiro, 7-Oct-2016.)
Hypotheses
Ref Expression
nfral.1 𝑥𝐴
nfral.2 𝑥𝜑
Assertion
Ref Expression
nfral 𝑥𝑦𝐴 𝜑

Proof of Theorem nfral
StepHypRef Expression
1 nftru 1796 . . 3 𝑦
2 nfral.1 . . . 4 𝑥𝐴
32a1i 11 . . 3 (⊤ → 𝑥𝐴)
4 nfral.2 . . . 4 𝑥𝜑
54a1i 11 . . 3 (⊤ → Ⅎ𝑥𝜑)
61, 3, 5nfrald 3224 . 2 (⊤ → Ⅎ𝑥𝑦𝐴 𝜑)
76mptru 1535 1 𝑥𝑦𝐴 𝜑
Colors of variables: wff setvar class
Syntax hints:  wtru 1529  wnf 1775  wnfc 2961  wral 3138
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-13 2383  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143
This theorem is referenced by:  nfra2  3228  nfiing  4944  disjxun  5056  fiun  7635  f1iun  7636  opreu2reuALT  30168  bnj1228  32181  poimirlem26  34800  poimirlem27  34801  eliuniincex  41256  disjinfi  41334  limsupre3uzlem  41896  xlimmnfv  41995  xlimpnfv  41999  stoweidlem51  42217  stoweidlem53  42219  stoweidlem54  42220  stoweidlem57  42223  stoweidlem59  42225  stoweidlem60  42226  fourierdlem31  42304  fourierdlem73  42345  iundjiun  42623  meaiuninc3v  42647  issmfle  42903  issmfgt  42914  issmfge  42927  smfpimcc  42963  smfsup  42969  smfinf  42973  cbvral2  43182  2reu3  43190  2reu8i  43193  ichreuopeq  43482  reupr  43531  reuopreuprim  43535
  Copyright terms: Public domain W3C validator