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

Theorem nfcsb 3414
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 1600 . . 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 3413 . 2  |-  ( T. 
->  F/_ x [_ A  /  y ]_ B
)
76trud 1379 1  |-  F/_ x [_ A  /  y ]_ B
Colors of variables: wff setvar class
Syntax hints:   T. wtru 1371   F/_wnfc 2602   [_csb 3396
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-sbc 3295  df-csb 3397
This theorem is referenced by:  cbvralcsf  3428  cbvreucsf  3430  cbvrabcsf  3431  fmptcof  5987  mpt2mptsx  6748  dmmpt2ssx  6750  fmpt2x  6751  fmpt2co  6767  dfmpt2  6774  mpt2curryd  6899  fvmpt2curryd  6901  nfsum  13287  fsum2dlem  13356  fsumcom2  13360  fsumcn  20579  fsum2cn  20580  dvmptfsum  21581  itgsubst  21655  iundisj2f  26084  f1od2  26176  nfcprod  27569  fprod2dlem  27636  fprodcom2  27640  wdom2d2  29533  elfvmptrab1  30303  elovmpt2rab1  30308  dmmpt2ssx2  30876  cdlemkid  34919  cdlemk19x  34926  cdlemk11t  34929
  Copyright terms: Public domain W3C validator