ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  csbeq2i GIF version

Theorem csbeq2i 2999
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 9 . . 3 (⊤ → 𝐵 = 𝐶)
32csbeq2dv 2998 . 2 (⊤ → 𝐴 / 𝑥𝐵 = 𝐴 / 𝑥𝐶)
43mptru 1325 1 𝐴 / 𝑥𝐵 = 𝐴 / 𝑥𝐶
Colors of variables: wff set class
Syntax hints:   = wceq 1316  wtru 1317  csb 2975
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-11 1469  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-tru 1319  df-nf 1422  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-sbc 2883  df-csb 2976
This theorem is referenced by:  csbvarg  3000  csbnest1g  3025  csbsng  3554  csbunig  3714  csbxpg  4590  csbcnvg  4693  csbdmg  4703  csbresg  4792  csbrng  4970  csbfv12g  5425  csbnegg  7928  iseqf1olemjpcl  10236  iseqf1olemqpcl  10237  iseqf1olemfvp  10238  seq3f1olemqsum  10241
  Copyright terms: Public domain W3C validator