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

Theorem nfcsb 3517
 Description: Bound-variable hypothesis builder for substitution into a class. (Contributed by Mario Carneiro, 12-Oct-2016.)
Hypotheses
Ref Expression
nfcsb.1 𝑥𝐴
nfcsb.2 𝑥𝐵
Assertion
Ref Expression
nfcsb 𝑥𝐴 / 𝑦𝐵

Proof of Theorem nfcsb
StepHypRef Expression
1 nftru 1721 . . 3 𝑦
2 nfcsb.1 . . . 4 𝑥𝐴
32a1i 11 . . 3 (⊤ → 𝑥𝐴)
4 nfcsb.2 . . . 4 𝑥𝐵
54a1i 11 . . 3 (⊤ → 𝑥𝐵)
61, 3, 5nfcsbd 3516 . 2 (⊤ → 𝑥𝐴 / 𝑦𝐵)
76trud 1484 1 𝑥𝐴 / 𝑦𝐵
 Colors of variables: wff setvar class Syntax hints:  ⊤wtru 1476  Ⅎwnfc 2738  ⦋csb 3499 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-sbc 3403  df-csb 3500 This theorem is referenced by:  cbvralcsf  3531  cbvreucsf  3533  cbvrabcsf  3534  elfvmptrab1  6213  fmptcof  6304  elovmpt2rab1  6779  mpt2mptsx  7122  dmmpt2ssx  7124  fmpt2x  7125  el2mpt2csbcl  7137  fmpt2co  7147  dfmpt2  7154  mpt2curryd  7282  fvmpt2curryd  7284  nfsum  14269  fsum2dlem  14343  fsumcom2  14347  fsumcom2OLD  14348  nfcprod  14480  fprod2dlem  14549  fprodcom2  14553  fprodcom2OLD  14554  fsumcn  22481  fsum2cn  22482  dvmptfsum  23542  itgsubst  23616  iundisj2f  28785  f1od2  28887  esumiun  29483  poimirlem26  32605  cdlemkid  35242  cdlemk19x  35249  cdlemk11t  35252  wdom2d2  36620  dmmpt2ssx2  41908
 Copyright terms: Public domain W3C validator