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

Theorem nfcsb 3228
Description: Bound-variable hypothesis builder for substitution into a class. (Contributed by Mario Carneiro, 12-Oct-2016.)
Hypotheses
Ref Expression
nfcsb.1  |-  F/_ x A
nfcsb.2  |-  F/_ x B
Assertion
Ref Expression
nfcsb  |-  F/_ x [_ A  /  y ]_ B

Proof of Theorem nfcsb
StepHypRef Expression
1 nftru 1560 . . 3  |-  F/ y  T.
2 nfcsb.1 . . . 4  |-  F/_ x A
32a1i 11 . . 3  |-  (  T. 
->  F/_ x A )
4 nfcsb.2 . . . 4  |-  F/_ x B
54a1i 11 . . 3  |-  (  T. 
->  F/_ x B )
61, 3, 5nfcsbd 3227 . 2  |-  (  T. 
->  F/_ x [_ A  /  y ]_ B
)
76trud 1329 1  |-  F/_ x [_ A  /  y ]_ B
Colors of variables: wff set class
Syntax hints:    T. wtru 1322   F/_wnfc 2510   [_csb 3194
This theorem is referenced by:  cbvralcsf  3254  cbvreucsf  3256  cbvrabcsf  3257  fmptcof  5841  mpt2mptsx  6353  dmmpt2ssx  6355  fmpt2x  6356  fmpt2co  6369  dfmpt2  6376  nfsum  12412  fsum2dlem  12481  fsumcom2  12485  fsumcn  18771  fsum2cn  18772  dvmptfsum  19726  itgsubst  19800  iundisj2f  23873  nfcprod  25016  wdom2d2  26797  cdlemkid  31050  cdlemk19x  31057  cdlemk11t  31060
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-sbc 3105  df-csb 3195
  Copyright terms: Public domain W3C validator