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

Theorem nfral 2790
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  |-  F/_ x A
nfral.2  |-  F/ x ph
Assertion
Ref Expression
nfral  |-  F/ x A. y  e.  A  ph

Proof of Theorem nfral
StepHypRef Expression
1 nftru 1599 . . 3  |-  F/ y T.
2 nfral.1 . . . 4  |-  F/_ x A
32a1i 11 . . 3  |-  ( T. 
->  F/_ x A )
4 nfral.2 . . . 4  |-  F/ x ph
54a1i 11 . . 3  |-  ( T. 
->  F/ x ph )
61, 3, 5nfrald 2788 . 2  |-  ( T. 
->  F/ x A. y  e.  A  ph )
76trud 1378 1  |-  F/ x A. y  e.  A  ph
Colors of variables: wff setvar class
Syntax hints:   T. wtru 1370   F/wnf 1589   F/_wnfc 2575   A.wral 2736
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ral 2741
This theorem is referenced by:  nfra2  2791  nfrex  2792  rspc2  3099  sbcralt  3288  raaan  3808  nfint  4159  nfiin  4220  disjxun  4311  nfpo  4667  nfso  4668  nffr  4715  nfse  4716  ralxpf  5007  dff13f  5994  nfiso  6036  mpt2eq123  6166  fun11iun  6558  fmpt2x  6661  ovmptss  6675  nfrecs  6855  xpf1o  7494  ac6sfi  7577  nfoi  7749  scottexs  8115  scott0s  8116  lble  10303  nnwof  10942  fzrevral  11565  rlimcld2  13077  fsum2dlem  13258  fsumcom2  13262  cnmpt21  19266  cfilucfilOLD  20166  cfilucfil  20167  ulmss  21884  fsumdvdscom  22547  dchrisumlema  22759  dchrisumlem2  22761  cnlnadjlem5  25497  disjabrex  25948  disjabrexf  25949  ordtconlem1  26376  untsucf  27383  fprod2dlem  27513  fprodcom2  27517  setinds  27613  tfisg  27687  wfisg  27692  frinsg  27728  nfwrecs  27741  indexdom  28654  filbcmb  28660  sdclem1  28665  scottexf  29006  scott0f  29007  setindtrs  29400  evth2f  29763  evthf  29775  climinff  29810  stoweidlem31  29852  stoweidlem34  29855  stoweidlem35  29856  stoweidlem51  29872  stoweidlem53  29874  stoweidlem54  29875  stoweidlem57  29878  stoweidlem59  29880  stoweidlem60  29881  cbvral2  30022  raaan2  30025  2reu3  30038  gsummoncoe1  30876  bnj1366  31919  bnj1385  31922  bnj981  32039  bnj1228  32098  bnj1398  32121  bnj1445  32131  bnj1449  32135  bnj1463  32142  cdleme31sn1  34121  cdlemk36  34653
  Copyright terms: Public domain W3C validator