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

Theorem nfcsb 3128
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 1544 . . 3  |-  F/ y  T.
2 nfcsb.1 . . . 4  |-  F/_ x A
32a1i 10 . . 3  |-  (  T. 
->  F/_ x A )
4 nfcsb.2 . . . 4  |-  F/_ x B
54a1i 10 . . 3  |-  (  T. 
->  F/_ x B )
61, 3, 5nfcsbd 3127 . 2  |-  (  T. 
->  F/_ x [_ A  /  y ]_ B
)
76trud 1314 1  |-  F/_ x [_ A  /  y ]_ B
Colors of variables: wff set class
Syntax hints:    T. wtru 1307   F/_wnfc 2419   [_csb 3094
This theorem is referenced by:  cbvralcsf  3156  cbvreucsf  3158  cbvrabcsf  3159  fmptcof  5708  mpt2mptsx  6203  dmmpt2ssx  6205  fmpt2x  6206  fmpt2co  6218  dfmpt2  6225  nfsum  12180  fsum2dlem  12249  fsumcom2  12253  fsumcn  18390  fsum2cn  18391  dvmptfsum  19338  itgsubst  19412  iundisj2f  23381  nfcprod  24133  wdom2d2  27231  cdlemkid  31747  cdlemk19x  31754  cdlemk11t  31757
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-sbc 3005  df-csb 3095
  Copyright terms: Public domain W3C validator