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

Theorem nfcsb 3419
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 1673 . . 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 3418 . 2  |-  ( T. 
->  F/_ x [_ A  /  y ]_ B
)
76trud 1446 1  |-  F/_ x [_ A  /  y ]_ B
Colors of variables: wff setvar class
Syntax hints:   T. wtru 1438   F/_wnfc 2577   [_csb 3401
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-sbc 3306  df-csb 3402
This theorem is referenced by:  cbvralcsf  3433  cbvreucsf  3435  cbvrabcsf  3436  elfvmptrab1  5986  fmptcof  6072  elovmpt2rab1  6530  mpt2mptsx  6870  dmmpt2ssx  6872  fmpt2x  6873  fmpt2co  6890  dfmpt2  6897  mpt2curryd  7024  fvmpt2curryd  7026  nfsum  13735  fsum2dlem  13809  fsumcom2  13813  nfcprod  13943  fprod2dlem  14012  fprodcom2  14016  fsumcn  21798  fsum2cn  21799  dvmptfsum  22804  itgsubst  22878  iundisj2f  28039  f1od2  28152  esumiun  28754  poimirlem26  31670  cdlemkid  34212  cdlemk19x  34219  cdlemk11t  34222  wdom2d2  35596  dmmpt2ssx2  38878
  Copyright terms: Public domain W3C validator