Theorem sbequ 1893

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 1892	. 2 ⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 → [𝑦 / 𝑧]𝜑))
2		sbequi 1892	. . 3 ⊢ (𝑦 = 𝑥 → ([𝑦 / 𝑧]𝜑 → [𝑥 / 𝑧]𝜑))
3	2	equcoms 1760	. 2 ⊢ (𝑥 = 𝑦 → ([𝑦 / 𝑧]𝜑 → [𝑥 / 𝑧]𝜑))
4	1, 3	impbid 129	1 ⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 ↔ [𝑦 / 𝑧]𝜑))

This proof depends on syntax axioms:   → wi 4   ↔ wb 105  [wsb 1815

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816

This theorem is used by:  drsb2  1894  sbco2vlem  2004  sbco2v  2008  sbco2yz  2023  sbcocom  2030  sb10f  2055  hbsb4  2072  nfsb4or  2081  sb8eu  2099  sb8euh  2109  cbvab  2364  cbvralf  2777  cbvrexf  2778  cbvreu  2784  cbvralsv  2802  cbvrexsv  2803  cbvrab  2819  cbvreucsf  3212  cbvrabcsf  3213  sbss  3635  disjiun  4125  cbvopab1  4204  cbvmpt  4226  tfis  4730  findes  4750  cbviota  5342  sb8iota  5345  cbvriota  6050  modom  7108  uzind4s  9990  bezoutlemmain  12775  cbvrald  16816  setindft  16991