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

Theorem nfral 2596
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 1541 . . 3  |-  F/ y  T.
2 nfral.1 . . . 4  |-  F/_ x A
32a1i 10 . . 3  |-  (  T. 
->  F/_ x A )
4 nfral.2 . . . 4  |-  F/ x ph
54a1i 10 . . 3  |-  (  T. 
->  F/ x ph )
61, 3, 5nfrald 2594 . 2  |-  (  T. 
->  F/ x A. y  e.  A  ph )
76trud 1314 1  |-  F/ x A. y  e.  A  ph
Colors of variables: wff set class
Syntax hints:    T. wtru 1307   F/wnf 1531   F/_wnfc 2406   A.wral 2543
This theorem is referenced by:  nfra2  2597  nfrex  2598  rspc2  2889  sbcralt  3063  sbcralg  3065  raaan  3561  nfint  3872  nfiin  3932  disjxun  4021  nfpo  4319  nfso  4320  nffr  4367  nfse  4368  ralxpf  4830  fun11iun  5493  dff13f  5784  nfiso  5821  mpt2eq123  5907  nfofr  6084  fmpt2x  6190  ovmptss  6200  nfrecs  6390  xpf1o  7023  ac6sfi  7101  nfoi  7229  scottexs  7557  scott0s  7558  lble  9706  nnwof  10285  fzrevral  10866  rlimcld2  12052  fsum2dlem  12233  fsumcom2  12237  cnmpt21  17365  ulmss  19774  fsumdvdscom  20425  dchrisumlema  20637  dchrisumlem2  20639  cnlnadjlem5  22651  disjabrex  23359  disjabrexf  23360  untsucf  24056  dedekind  24082  dedekindle  24083  setinds  24134  tfisg  24204  wfisg  24209  frinsg  24245  imonclem  25813  cmpmon  25815  iepiclem  25823  indexdom  26413  filbcmb  26432  sdclem1  26453  setindtrs  27118  evth2f  27686  evthf  27698  climinff  27737  stoweidlem31  27780  stoweidlem34  27783  stoweidlem35  27784  stoweidlem51  27800  stoweidlem53  27802  stoweidlem54  27803  stoweidlem57  27806  stoweidlem59  27808  stoweidlem60  27809  cbvral2  27950  raaan2  27953  2reu3  27966  bnj1366  28862  bnj1379  28863  bnj1385  28865  bnj981  28982  bnj1228  29041  bnj1398  29064  bnj1445  29074  bnj1449  29078  bnj1463  29085  cdleme31sn1  30570  cdlemk36  31102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ral 2548
  Copyright terms: Public domain W3C validator