NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  sbequ GIF version

Theorem sbequ 2060
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 2059 . 2 (x = y → ([x / z]φ → [y / z]φ))
2 sbequi 2059 . . 3 (y = x → ([y / z]φ → [x / z]φ))
32equcoms 1681 . 2 (x = y → ([y / z]φ → [x / z]φ))
41, 3impbid 183 1 (x = y → ([x / z]φ ↔ [y / z]φ))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 176  [wsb 1648
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649
This theorem is referenced by:  drsb2  2061  sbco2  2086  sb10f  2122  sb8eu  2222  cbvab  2471  cbvralf  2829  cbvreu  2833  cbvralsv  2846  cbvrexsv  2847  cbvrab  2857  cbvreucsf  3200  cbvrabcsf  3201  sbss  3659  cbviota  4344  sb8iota  4346  cbvopab1  4632  cbvmpt  5676
  Copyright terms: Public domain W3C validator