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

Theorem csbeq2i 4219
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 4218 . 2 (⊤ → 𝐴 / 𝑥𝐵 = 𝐴 / 𝑥𝐶)
43mptru 1664 1 𝐴 / 𝑥𝐵 = 𝐴 / 𝑥𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1656  wtru 1657  csb 3757
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-ext 2803
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-clab 2812  df-cleq 2818  df-clel 2821  df-sbc 3663  df-csb 3758
This theorem is referenced by:  csbnest1g  4227  csbvarg  4229  csbsng  4464  csbprg  4465  csbopg  4643  csbuni  4690  csbmpt12  5238  csbxp  5439  csbcnv  5542  csbcnvgALT  5543  csbdm  5554  csbres  5636  csbrn  5841  csbfv12  6481  fvmpt2curryd  7667  csbnegg  10605  csbwrdg  13611  matgsum  20617  disjxpin  29944  f1od2  30043  bj-csbsn  33419  csbpredg  33717  csbwrecsg  33718  csbrecsg  33719  csbrdgg  33720  csboprabg  33721  csbmpt22g  33722  csbfinxpg  33769  poimirlem24  33976  cdleme31so  36453  cdleme31sn  36454  cdleme31sn1  36455  cdleme31se  36456  cdleme31se2  36457  cdleme31sc  36458  cdleme31sde  36459  cdleme31sn2  36463  cdlemkid3N  37007  cdlemkid4  37008  climinf2mpt  40739  climinfmpt  40740
  Copyright terms: Public domain W3C validator