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

Theorem nfcsb 3692
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 1879 . . 3 𝑦
2 nfcsb.1 . . . 4 𝑥𝐴
32a1i 11 . . 3 (⊤ → 𝑥𝐴)
4 nfcsb.2 . . . 4 𝑥𝐵
54a1i 11 . . 3 (⊤ → 𝑥𝐵)
61, 3, 5nfcsbd 3691 . 2 (⊤ → 𝑥𝐴 / 𝑦𝐵)
76trud 1642 1 𝑥𝐴 / 𝑦𝐵
Colors of variables: wff setvar class
Syntax hints:  wtru 1633  wnfc 2889  csb 3674
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-sbc 3577  df-csb 3675
This theorem is referenced by:  cbvralcsf  3706  cbvreucsf  3708  cbvrabcsf  3709  elfvmptrab1  6467  fmptcof  6560  elovmpt2rab1  7046  mpt2mptsx  7401  dmmpt2ssx  7403  fmpt2x  7404  el2mpt2csbcl  7418  fmpt2co  7428  dfmpt2  7435  mpt2curryd  7564  fvmpt2curryd  7566  nfsum  14620  fsum2dlem  14700  fsumcom2  14704  fsumcom2OLD  14705  nfcprod  14840  fprod2dlem  14909  fprodcom2  14913  fprodcom2OLD  14914  fsumcn  22874  fsum2cn  22875  dvmptfsum  23937  itgsubst  24011  iundisj2f  29710  f1od2  29808  esumiun  30465  poimirlem26  33748  cdlemkid  36726  cdlemk19x  36733  cdlemk11t  36736  wdom2d2  38104  dmmpt2ssx2  42625
  Copyright terms: Public domain W3C validator