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

Theorem csbeq2i 4187
Description: Formula-building inference for class substitution. (Contributed by NM, 10-Nov-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
Hypothesis
Ref Expression
csbeq2i.1 𝐵 = 𝐶
Assertion
Ref Expression
csbeq2i 𝐴 / 𝑥𝐵 = 𝐴 / 𝑥𝐶

Proof of Theorem csbeq2i
StepHypRef Expression
1 csbeq2i.1 . . . 4 𝐵 = 𝐶
21a1i 11 . . 3 (⊤ → 𝐵 = 𝐶)
32csbeq2dv 4186 . 2 (⊤ → 𝐴 / 𝑥𝐵 = 𝐴 / 𝑥𝐶)
43mptru 1661 1 𝐴 / 𝑥𝐵 = 𝐴 / 𝑥𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1653  wtru 1654  csb 3727
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2776
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2785  df-cleq 2791  df-clel 2794  df-sbc 3633  df-csb 3728
This theorem is referenced by:  csbnest1g  4195  csbvarg  4197  csbsng  4432  csbprg  4433  csbopg  4610  csbuni  4657  csbmpt12  5205  csbxp  5404  csbcnv  5508  csbcnvgALT  5509  csbdm  5520  csbres  5602  csbrn  5811  csbfv12  6454  fvmpt2curryd  7634  csbnegg  10568  csbwrdg  13561  matgsum  20565  disjxpin  29911  f1od2  30010  bj-csbsn  33383  csbpredg  33664  csbwrecsg  33665  csbrecsg  33666  csbrdgg  33667  csboprabg  33668  csbmpt22g  33669  csbfinxpg  33716  poimirlem24  33915  cdleme31so  36393  cdleme31sn  36394  cdleme31sn1  36395  cdleme31se  36396  cdleme31se2  36397  cdleme31sc  36398  cdleme31sde  36399  cdleme31sn2  36403  cdlemkid3N  36947  cdlemkid4  36948  climinf2mpt  40679  climinfmpt  40680
  Copyright terms: Public domain W3C validator