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

Theorem csbeq2i 3970
Description: Formula-building inference rule 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 3969 . 2 (⊤ → 𝐴 / 𝑥𝐵 = 𝐴 / 𝑥𝐶)
43trud 1490 1 𝐴 / 𝑥𝐵 = 𝐴 / 𝑥𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1480  wtru 1481  csb 3518
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-sbc 3422  df-csb 3519
This theorem is referenced by:  csbnest1g  3978  csbvarg  3980  csbsng  4219  csbprg  4220  csbopg  4393  csbuni  4437  csbmpt12  4975  csbxp  5166  csbcnv  5271  csbcnvgALT  5272  csbdm  5283  csbres  5364  csbrn  5560  csbfv12  6193  fvmpt2curryd  7349  csbnegg  10230  csbwrdg  13281  matgsum  20175  disjxpin  29269  bj-csbsn  32581  csbpredg  32839  csbwrecsg  32840  csbrecsg  32841  csbrdgg  32842  csboprabg  32843  csbmpt22g  32844  csbfinxpg  32892  poimirlem24  33100  cdleme31so  35182  cdleme31sn  35183  cdleme31sn1  35184  cdleme31se  35185  cdleme31se2  35186  cdleme31sc  35187  cdleme31sde  35188  cdleme31sn2  35192  cdlemkid3N  35736  cdlemkid4  35737  csbunigOLD  38569  csbfv12gALTOLD  38570  csbxpgOLD  38571  csbresgOLD  38573  csbrngOLD  38574  csbima12gALTOLD  38575  climinf2mpt  39378  climinfmpt  39379
  Copyright terms: Public domain W3C validator