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

Step	Hyp	Ref	Expression
1		sbequi 2059	. 2 ⊢ (x = y → ([x / z]φ → [y / z]φ))
2		sbequi 2059	. . 3 ⊢ (y = x → ([y / z]φ → [x / z]φ))
3	2	equcoms 1681	. 2 ⊢ (x = y → ([y / z]φ → [x / z]φ))
4	1, 3	impbid 183	1 ⊢ (x = y → ([x / z]φ ↔ [y / z]φ))

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  2472  cbvralf  2830  cbvreu  2834  cbvralsv  2847  cbvrexsv  2848  cbvrab  2858  cbvreucsf  3201  cbvrabcsf  3202  sbss  3660  cbviota  4345  sb8iota  4347  cbvopab1  4633  cbvmpt  5677