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-1 5  ax-2 6  ax-3 7  ax-mp 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