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 2249 | . . 3 ⊢ (𝑦 = 𝑥 → (𝜑 ↔ [𝑥 / 𝑦]𝜑)) | |
2 | 1 | bicomd 226 | . 2 ⊢ (𝑦 = 𝑥 → ([𝑥 / 𝑦]𝜑 ↔ 𝜑)) |
3 | 2 | equcoms 2028 | 1 ⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑦]𝜑 ↔ 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 [wsb 2070 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-12 2175 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1788 df-sb 2071 |
This theorem is referenced by: sbelx 2251 sbequ12a 2252 sbid 2253 sbid2vw 2256 sb6rfv 2356 sbbib 2360 sb5rf 2466 sb6rf 2467 2sb5rf 2471 2sb6rf 2472 abbi 2810 opeliunxp 5616 isarep1 6468 findes 7680 axrepndlem1 10206 axrepndlem2 10207 nn0min 30854 esumcvg 31766 bj-sbidmOLD 34771 bj-gabima 34865 wl-nfs1t 35433 wl-sb6rft 35440 wl-equsb4 35449 wl-ax11-lem5 35477 sbcalf 36009 sbcexf 36010 opeliun2xp 45341 |
Copyright terms: Public domain | W3C validator |