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

Theorem sbequ 1813
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 1812 . 2 (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 → [𝑦 / 𝑧]𝜑))
2 sbequi 1812 . . 3 (𝑦 = 𝑥 → ([𝑦 / 𝑧]𝜑 → [𝑥 / 𝑧]𝜑))
32equcoms 1685 . 2 (𝑥 = 𝑦 → ([𝑦 / 𝑧]𝜑 → [𝑥 / 𝑧]𝜑))
41, 3impbid 128 1 (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 ↔ [𝑦 / 𝑧]𝜑))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104  [wsb 1736
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-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516
This theorem depends on definitions:  df-bi 116  df-nf 1438  df-sb 1737
This theorem is referenced by:  drsb2  1814  sbco2vlem  1918  sbco2v  1922  sbco2yz  1937  sbcocom  1944  sb10f  1971  hbsb4  1988  nfsb4or  1999  sb8eu  2013  sb8euh  2023  cbvab  2264  cbvralf  2651  cbvrexf  2652  cbvreu  2655  cbvralsv  2671  cbvrexsv  2672  cbvrab  2687  cbvreucsf  3068  cbvrabcsf  3069  sbss  3475  disjiun  3931  cbvopab1  4008  cbvmpt  4030  tfis  4504  findes  4524  cbviota  5100  sb8iota  5102  cbvriota  5747  uzind4s  9411  bezoutlemmain  11720  cbvrald  13164  setindft  13332
  Copyright terms: Public domain W3C validator