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

Theorem sbequ 1699
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 (x = y → ([x / z]φ ↔ [y / z]φ))

Proof of Theorem sbequ
StepHypRef Expression
1 sbequi 1698 . 2 (x = y → ([x / z]φ → [y / z]φ))
2 sbequi 1698 . . 3 (y = x → ([y / z]φ → [x / z]φ))
32equcoms 1572 . 2 (x = y → ([y / z]φ → [x / z]φ))
41, 3impbid 120 1 (x = y → ([x / z]φ ↔ [y / z]φ))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98  [wsb 1623
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 617  ax-5 1312  ax-7 1313  ax-gen 1314  ax-ie1 1359  ax-ie2 1360  ax-8 1372  ax-10 1373  ax-11 1374  ax-i12 1375  ax-4 1377  ax-17 1396  ax-i9 1400  ax-ial 1405  ax-i5r 1406
This theorem depends on definitions:  df-bi 110  df-nf 1326  df-sb 1624
This theorem is referenced by:  drsb2  1700  sbco2vlem  1798  sbco2yz  1815  sbcocom  1822  sb10f  1849  hbsb4  1866  nfsb4or  1877  sb8eu  1891  sb8euh  1901  cbvab  2138  cbvralf  2501  cbvrexf  2502  cbvreu  2505  cbvralsv  2518  cbvrexsv  2519  cbvrab  2529  cbvreucsf  2883  cbvrabcsf  2884  sbss  3304  cbvopab1  3800  cbvmpt  3821  tfis  4229  findes  4249  cbviota  4795  sb8iota  4797  cbvriota  5398  cbvrald  7173  setindft  7322
  Copyright terms: Public domain W3C validator