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

Theorem nfral 3231
 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 1798 . . 3 𝑦
2 nfral.1 . . . 4 𝑥𝐴
32a1i 11 . . 3 (⊤ → 𝑥𝐴)
4 nfral.2 . . . 4 𝑥𝜑
54a1i 11 . . 3 (⊤ → Ⅎ𝑥𝜑)
61, 3, 5nfrald 3229 . 2 (⊤ → Ⅎ𝑥𝑦𝐴 𝜑)
76mptru 1537 1 𝑥𝑦𝐴 𝜑
 Colors of variables: wff setvar class Syntax hints:  ⊤wtru 1531  Ⅎwnf 1777  Ⅎwnfc 2966  ∀wral 3143 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-13 2385  ax-ext 2798 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ral 3148 This theorem is referenced by:  nfra2  3233  nfiing  4949  disjxun  5061  fiun  7640  f1iun  7641  opreu2reuALT  30173  disjabrex  30266  disjabrexf  30267  aciunf1lem  30341  fnpreimac  30350  fsumiunle  30478  ordtconnlem1  31072  esumiun  31258  bnj1366  32006  bnj1385  32009  bnj981  32127  bnj1228  32186  bnj1398  32209  bnj1445  32219  bnj1449  32223  bnj1463  32230  setinds  32926  tfisg  32958  frpoinsg  32984  frinsg  32990  nffrecs  33023  nosupbnd1  33117  poimirlem26  34804  poimirlem27  34805  indexdom  34896  filbcmb  34902  sdclem1  34905  scottexf  35333  scott0f  35334  cdleme31sn1  37403  cdlemk36  37935  nfscott  40459  scottabf  40460  evth2f  41156  evthf  41168  uzwo4  41199  eliuniincex  41260  disjinfi  41338  choicefi  41347  rnmptbd2lem  41404  rnmptbdlem  41411  ssfiunibd  41460  infxrunb2  41520  supxrunb3  41556  supxrleubrnmpt  41563  allbutfiinf  41578  suprleubrnmpt  41580  infxrgelbrnmpt  41614  climinff  41776  limsupre3uzlem  41900  xlimmnfv  41999  xlimpnfv  42003  cncfshift  42041  cncficcgt0  42055  stoweidlem31  42201  stoweidlem34  42204  stoweidlem35  42205  stoweidlem51  42221  stoweidlem53  42223  stoweidlem54  42224  stoweidlem57  42227  stoweidlem59  42229  stoweidlem60  42230  fourierdlem31  42308  fourierdlem73  42349  iundjiun  42627  meaiuninc3v  42651  issmfle  42907  issmfgt  42918  issmfge  42931  smfpimcc  42967  smfsup  42973  smfinf  42977  cbvral2  43186  2reu3  43194  2reu8i  43197  ichreuopeq  43486  reupr  43535  reuopreuprim  43539
 Copyright terms: Public domain W3C validator