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

Theorem nfcsb 3458
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 1609 . . 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 3457 . 2  |-  ( T. 
->  F/_ x [_ A  /  y ]_ B
)
76trud 1388 1  |-  F/_ x [_ A  /  y ]_ B
Colors of variables: wff setvar class
Syntax hints:   T. wtru 1380   F/_wnfc 2615   [_csb 3440
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-sbc 3337  df-csb 3441
This theorem is referenced by:  cbvralcsf  3472  cbvreucsf  3474  cbvrabcsf  3475  elfvmptrab1  5977  fmptcof  6066  elovmpt2rab1  6517  mpt2mptsx  6858  dmmpt2ssx  6860  fmpt2x  6861  fmpt2co  6878  dfmpt2  6885  mpt2curryd  7010  fvmpt2curryd  7012  nfsum  13493  fsum2dlem  13565  fsumcom2  13569  fsumcn  21242  fsum2cn  21243  dvmptfsum  22244  itgsubst  22318  iundisj2f  27263  f1od2  27361  nfcprod  28961  fprod2dlem  29028  fprodcom2  29032  wdom2d2  30896  dmmpt2ssx2  32360  cdlemkid  36088  cdlemk19x  36095  cdlemk11t  36098
  Copyright terms: Public domain W3C validator