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

Theorem nfcsb 3709
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 1899 . . 3 𝑦
2 nfcsb.1 . . . 4 𝑥𝐴
32a1i 11 . . 3 (⊤ → 𝑥𝐴)
4 nfcsb.2 . . . 4 𝑥𝐵
54a1i 11 . . 3 (⊤ → 𝑥𝐵)
61, 3, 5nfcsbd 3708 . 2 (⊤ → 𝑥𝐴 / 𝑦𝐵)
76mptru 1660 1 𝑥𝐴 / 𝑦𝐵
Colors of variables: wff setvar class
Syntax hints:  wtru 1653  wnfc 2894  csb 3691
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-sbc 3597  df-csb 3692
This theorem is referenced by:  cbvralcsf  3723  cbvreucsf  3725  cbvrabcsf  3726  elfvmptrab1  6494  fmptcof  6588  elovmpt2rab1  7079  mpt2mptsx  7434  dmmpt2ssx  7436  fmpt2x  7437  el2mpt2csbcl  7451  fmpt2co  7462  dfmpt2  7469  mpt2curryd  7598  fvmpt2curryd  7600  nfsum  14706  fsum2dlem  14786  fsumcom2  14790  nfcprod  14924  fprod2dlem  14993  fprodcom2  14997  fsumcn  22952  fsum2cn  22953  dvmptfsum  24029  itgsubst  24103  iundisj2f  29851  f1od2  29948  esumiun  30603  poimirlem26  33859  cdlemkid  36892  cdlemk19x  36899  cdlemk11t  36902  wdom2d2  38279  dmmpt2ssx2  42784
  Copyright terms: Public domain W3C validator