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

Theorem csbeq2i 3863
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 3862 . 2 (⊤ → 𝐴 / 𝑥𝐵 = 𝐴 / 𝑥𝐶)
43mptru 1570 1 𝐴 / 𝑥𝐵 = 𝐴 / 𝑥𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1563  wtru 1564  csb 3855
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737
This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-sbc 3748  df-csb 3856
This theorem is referenced by:  csbnest1g  4389  csbvarg  4391  csbsng  4670  csbprg  4671  csbopg  4852  csbuni  4899  csbmpt12  5533  csbxp  5753  csbcnv  5863  csbcnvOLD  5864  csbcnvgALTOLD  5865  csbdm  5878  csbres  5972  csbrn  6194  csbpredg  6298  csbfv12  6916  fvmpocurryd  8255  csbfrecsg  8269  csbwrecsg  8303  csbnegg  11442  csbwrdg  14571  matgsum  22555  precsexlemcbv  28357  precsexlem3  28360  disjxpin  32843  f1od2  32976  sumeq2si  36575  prodeq2si  36577  bj-csbsn  37401  csbrecsg  37834  csbrdgg  37835  csboprabg  37836  csbmpo123  37837  csbfinxpg  37894  poimirlem24  38155  cdleme31so  41015  cdleme31sn  41016  cdleme31sn1  41017  cdleme31se  41018  cdleme31se2  41019  cdleme31sc  41020  cdleme31sde  41021  cdleme31sn2  41025  cdlemkid3N  41569  cdlemkid4  41570  climinf2mpt  46286  climinfmpt  46287
  Copyright terms: Public domain W3C validator