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

Theorem sbequ 1765
Description: An equality theorem for substitution. Used in proof of Theorem 9.7 in [Megill] p. 449 (p. 16 of the preprint). (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
sbequ (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 ↔ [𝑦 / 𝑧]𝜑))

Proof of Theorem sbequ
StepHypRef Expression
1 sbequi 1764 . 2 (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 → [𝑦 / 𝑧]𝜑))
2 sbequi 1764 . . 3 (𝑦 = 𝑥 → ([𝑦 / 𝑧]𝜑 → [𝑥 / 𝑧]𝜑))
32equcoms 1638 . 2 (𝑥 = 𝑦 → ([𝑦 / 𝑧]𝜑 → [𝑥 / 𝑧]𝜑))
41, 3impbid 127 1 (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 ↔ [𝑦 / 𝑧]𝜑))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103  [wsb 1689
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471
This theorem depends on definitions:  df-bi 115  df-nf 1393  df-sb 1690
This theorem is referenced by:  drsb2  1766  sbco2vlem  1865  sbco2yz  1882  sbcocom  1889  sb10f  1916  hbsb4  1933  nfsb4or  1944  sb8eu  1958  sb8euh  1968  cbvab  2207  cbvralf  2580  cbvrexf  2581  cbvreu  2584  cbvralsv  2597  cbvrexsv  2598  cbvrab  2613  cbvreucsf  2981  cbvrabcsf  2982  sbss  3377  cbvopab1  3888  cbvmpt  3910  tfis  4373  findes  4393  cbviota  4953  sb8iota  4955  cbvriota  5581  uzind4s  9013  bezoutlemmain  10912  cbvrald  11176  setindft  11348
  Copyright terms: Public domain W3C validator