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

Theorem nfral 2751
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 1671 . . 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 2750 . 2  |-  ( T. 
->  F/ x A. y  e.  A  ph )
76trud 1446 1  |-  F/ x A. y  e.  A  ph
Colors of variables: wff setvar class
Syntax hints:   T. wtru 1438   F/wnf 1661   F/_wnfc 2556   A.wral 2714
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-cleq 2421  df-clel 2424  df-nfc 2558  df-ral 2719
This theorem is referenced by:  nfra2  2752  nfrexOLD  2828  rspc2  3133  sbcralt  3315  raaan  3850  nfint  4208  nfiin  4271  disjxun  4364  nfpo  4722  nfso  4723  nffr  4770  nfse  4771  ralxpf  4943  wfisg  5377  dff13f  6119  nfiso  6174  mpt2eq123  6308  fun11iun  6711  fmpt2x  6817  ovmptss  6832  nfwrecs  6985  xpf1o  7687  ac6sfi  7768  nfoi  7982  scottexs  8310  scott0s  8311  lble  10509  nnwof  11176  fzrevral  11830  rlimcld2  13585  fsum2dlem  13774  fsumcom2  13778  fprod2dlem  13977  fprodcom2  13981  gsummoncoe1  18841  cnmpt21  20628  cfilucfil  21516  ulmss  23294  fsumdvdscom  24056  dchrisumlema  24268  dchrisumlem2  24270  cnlnadjlem5  27666  disjabrex  28138  disjabrexf  28139  aciunf1lem  28210  ordtconlem1  28682  esumiun  28867  bnj1366  29593  bnj1385  29596  bnj981  29713  bnj1228  29772  bnj1398  29795  bnj1445  29805  bnj1449  29809  bnj1463  29816  untsucf  30289  setinds  30375  tfisg  30408  frinsg  30434  poimirlem26  31873  poimirlem27  31874  indexdom  31968  filbcmb  31974  sdclem1  31979  scottexf  32318  scott0f  32319  cdleme31sn1  33860  cdlemk36  34392  setindtrs  35793  evth2f  37252  evthf  37264  uzwo4  37308  disjinfi  37372  ssfiunibd  37424  climinff  37573  climinffOLD  37574  cncfshift  37634  cncficcgt0  37649  stoweidlem31  37775  stoweidlem34  37778  stoweidlem35  37779  stoweidlem51  37795  stoweidlem53  37797  stoweidlem54  37798  stoweidlem57  37801  stoweidlem59  37803  stoweidlem60  37804  fourierdlem31  37883  fourierdlem31OLD  37884  fourierdlem73  37926  iundjiun  38149  cbvral2  38407  raaan2  38410  2reu3  38423
  Copyright terms: Public domain W3C validator