| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > sbequ12r | Structured version Visualization version GIF version | ||
| Description: An equality theorem for substitution. (Contributed by NM, 6-Oct-2004.) (Proof shortened by Andrew Salmon, 21-Jun-2011.) |
| Ref | Expression |
|---|---|
| sbequ12r | ⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑦]𝜑 ↔ 𝜑)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sbequ12 2251 | . . 3 ⊢ (𝑦 = 𝑥 → (𝜑 ↔ [𝑥 / 𝑦]𝜑)) | |
| 2 | 1 | bicomd 223 | . 2 ⊢ (𝑦 = 𝑥 → ([𝑥 / 𝑦]𝜑 ↔ 𝜑)) |
| 3 | 2 | equcoms 2019 | 1 ⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑦]𝜑 ↔ 𝜑)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 [wsb 2064 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-12 2177 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-sb 2065 |
| This theorem is referenced by: sbelx 2253 sbequ12a 2254 sbid 2255 sbcov 2256 sbid2vw 2259 sb6rfv 2360 sbbib 2364 sb5rf 2472 sb6rf 2473 2sb5rf 2477 2sb6rf 2478 abbib 2811 opeliunxp 5752 opeliun2xp 5753 isarep1 6656 isarep1OLD 6657 findes 7922 axrepndlem1 10632 axrepndlem2 10633 nn0min 32822 esumcvg 34087 bj-sbidmOLD 36851 bj-gabima 36941 wl-nfs1t 37538 wl-sbid2ft 37546 wl-equsb4 37558 wl-ax11-lem5 37590 sbcalf 38121 sbcexf 38122 |
| Copyright terms: Public domain | W3C validator |