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

Theorem nfcsb 3584
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 1770 . . 3 𝑦
2 nfcsb.1 . . . 4 𝑥𝐴
32a1i 11 . . 3 (⊤ → 𝑥𝐴)
4 nfcsb.2 . . . 4 𝑥𝐵
54a1i 11 . . 3 (⊤ → 𝑥𝐵)
61, 3, 5nfcsbd 3583 . 2 (⊤ → 𝑥𝐴 / 𝑦𝐵)
76trud 1533 1 𝑥𝐴 / 𝑦𝐵
Colors of variables: wff setvar class
Syntax hints:  wtru 1524  wnfc 2780  csb 3566
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-sbc 3469  df-csb 3567
This theorem is referenced by:  cbvralcsf  3598  cbvreucsf  3600  cbvrabcsf  3601  elfvmptrab1  6344  fmptcof  6437  elovmpt2rab1  6923  mpt2mptsx  7278  dmmpt2ssx  7280  fmpt2x  7281  el2mpt2csbcl  7295  fmpt2co  7305  dfmpt2  7312  mpt2curryd  7440  fvmpt2curryd  7442  nfsum  14465  fsum2dlem  14545  fsumcom2  14549  fsumcom2OLD  14550  nfcprod  14685  fprod2dlem  14754  fprodcom2  14758  fprodcom2OLD  14759  fsumcn  22720  fsum2cn  22721  dvmptfsum  23783  itgsubst  23857  iundisj2f  29529  f1od2  29627  esumiun  30284  poimirlem26  33565  cdlemkid  36541  cdlemk19x  36548  cdlemk11t  36551  wdom2d2  37919  dmmpt2ssx2  42440
  Copyright terms: Public domain W3C validator