Theorem csbeq2i 3841

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

Step	Hyp	Ref	Expression
1		csbeq2i.1	. . . 4 ⊢ 𝐵 = 𝐶
2	1	a1i 11	. . 3 ⊢ (⊤ → 𝐵 = 𝐶)
3	2	csbeq2dv 3840	. 2 ⊢ (⊤ → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶)
4	3	mptru 1546	1 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶

Syntax hints:   = wceq 1539  ⊤wtru 1540  ⦋csb 3833

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-12 2172  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-sbc 3718  df-csb 3834

This theorem is referenced by:  csbnest1g  4364  csbvarg  4366  csbsng  4645  csbprg  4646  csbopg  4823  csbuni  4871  csbmpt12  5471  csbxp  5687  csbcnv  5795  csbcnvgALT  5796  csbdm  5809  csbres  5897  csbrn  6111  csbpredg  6212  csbfv12  6826  fvmpocurryd  8096  csbfrecsg  8109  csbwrecsg  8146  csbnegg  11227  csbwrdg  14256  matgsum  21595  disjxpin  30936  f1od2  31065  bj-csbsn  35098  csbrecsg  35508  csbrdgg  35509  csboprabg  35510  csbmpo123  35511  csbfinxpg  35568  poimirlem24  35810  cdleme31so  38400  cdleme31sn  38401  cdleme31sn1  38402  cdleme31se  38403  cdleme31se2  38404  cdleme31sc  38405  cdleme31sde  38406  cdleme31sn2  38410  cdlemkid3N  38954  cdlemkid4  38955  climinf2mpt  43262  climinfmpt  43263