![]() |
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 2252 | . . 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 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-12 2178 |
This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1778 df-sb 2065 |
This theorem is referenced by: sbelx 2254 sbequ12a 2255 sbid 2256 sbcov 2257 sbid2vw 2260 sb6rfv 2363 sbbib 2367 sb5rf 2475 sb6rf 2476 2sb5rf 2480 2sb6rf 2481 abbib 2814 opeliunxp 5767 isarep1 6667 isarep1OLD 6668 findes 7940 axrepndlem1 10661 axrepndlem2 10662 nn0min 32824 esumcvg 34050 bj-sbidmOLD 36816 bj-gabima 36906 wl-nfs1t 37491 wl-sbid2ft 37499 wl-equsb4 37511 wl-ax11-lem5 37543 sbcalf 38074 sbcexf 38075 opeliun2xp 48057 |
Copyright terms: Public domain | W3C validator |