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

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

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