Theorem sbequ 1889

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	⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 ↔ [𝑦 / 𝑧]𝜑))

Proof of Theorem sbequ

Step	Hyp	Ref	Expression
1		sbequi 1888	. 2 ⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 → [𝑦 / 𝑧]𝜑))
2		sbequi 1888	. . 3 ⊢ (𝑦 = 𝑥 → ([𝑦 / 𝑧]𝜑 → [𝑥 / 𝑧]𝜑))
3	2	equcoms 1756	. 2 ⊢ (𝑥 = 𝑦 → ([𝑦 / 𝑧]𝜑 → [𝑥 / 𝑧]𝜑))
4	1, 3	impbid 129	1 ⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 ↔ [𝑦 / 𝑧]𝜑))

Syntax hints:   → wi 4   ↔ wb 105  [wsb 1811

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812

This theorem is referenced by:  drsb2  1890  sbco2vlem  1998  sbco2v  2002  sbco2yz  2017  sbcocom  2024  sb10f  2049  hbsb4  2066  nfsb4or  2075  sb8eu  2093  sb8euh  2103  cbvab  2358  cbvralf  2769  cbvrexf  2770  cbvreu  2776  cbvralsv  2794  cbvrexsv  2795  cbvrab  2811  cbvreucsf  3203  cbvrabcsf  3204  sbss  3617  disjiun  4104  cbvopab1  4183  cbvmpt  4205  tfis  4705  findes  4725  cbviota  5317  sb8iota  5320  cbvriota  6015  modom  7061  uzind4s  9922  bezoutlemmain  12694  cbvrald  16560  setindft  16735