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

Theorem nfcsb 3516
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 1720 . . 3 𝑦
2 nfcsb.1 . . . 4 𝑥𝐴
32a1i 11 . . 3 (⊤ → 𝑥𝐴)
4 nfcsb.2 . . . 4 𝑥𝐵
54a1i 11 . . 3 (⊤ → 𝑥𝐵)
61, 3, 5nfcsbd 3515 . 2 (⊤ → 𝑥𝐴 / 𝑦𝐵)
76trud 1483 1 𝑥𝐴 / 𝑦𝐵
Colors of variables: wff setvar class
Syntax hints:  wtru 1475  wnfc 2737  csb 3498
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2232  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-sbc 3402  df-csb 3499
This theorem is referenced by:  cbvralcsf  3530  cbvreucsf  3532  cbvrabcsf  3533  elfvmptrab1  6198  fmptcof  6289  elovmpt2rab1  6756  mpt2mptsx  7099  dmmpt2ssx  7101  fmpt2x  7102  el2mpt2csbcl  7114  fmpt2co  7124  dfmpt2  7131  mpt2curryd  7259  fvmpt2curryd  7261  nfsum  14215  fsum2dlem  14289  fsumcom2  14293  fsumcom2OLD  14294  nfcprod  14426  fprod2dlem  14495  fprodcom2  14499  fprodcom2OLD  14500  fsumcn  22412  fsum2cn  22413  dvmptfsum  23459  itgsubst  23533  iundisj2f  28591  f1od2  28693  esumiun  29289  poimirlem26  32408  cdlemkid  35045  cdlemk19x  35052  cdlemk11t  35055  wdom2d2  36423  dmmpt2ssx2  41910
  Copyright terms: Public domain W3C validator