Theorem sbequ 1765

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

Syntax hints:   → wi 4   ↔ wb 103  [wsb 1689

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471

This theorem depends on definitions:  df-bi 115  df-nf 1393  df-sb 1690

This theorem is referenced by:  drsb2  1766  sbco2vlem  1865  sbco2yz  1882  sbcocom  1889  sb10f  1916  hbsb4  1933  nfsb4or  1944  sb8eu  1958  sb8euh  1968  cbvab  2207  cbvralf  2580  cbvrexf  2581  cbvreu  2584  cbvralsv  2597  cbvrexsv  2598  cbvrab  2613  cbvreucsf  2981  cbvrabcsf  2982  sbss  3377  cbvopab1  3888  cbvmpt  3910  tfis  4373  findes  4393  cbviota  4953  sb8iota  4955  cbvriota  5581  uzind4s  9013  bezoutlemmain  10912  cbvrald  11176  setindft  11348