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

Theorem nfcsb 3115
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 1541 . . 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 3114 . 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 2406   [_csb 3081
This theorem is referenced by:  cbvralcsf  3143  cbvreucsf  3145  cbvrabcsf  3146  fmptcof  5692  mpt2mptsx  6187  dmmpt2ssx  6189  fmpt2x  6190  fmpt2co  6202  dfmpt2  6209  nfsum  12164  fsum2dlem  12233  fsumcom2  12237  fsumcn  18374  fsum2cn  18375  dvmptfsum  19322  itgsubst  19396  iundisj2f  23366  wdom2d2  27128  cdlemkid  31125  cdlemk19x  31132  cdlemk11t  31135
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-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-sbc 2992  df-csb 3082
  Copyright terms: Public domain W3C validator