|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > sbequ12 | Structured version Visualization version GIF version | ||
| Description: An equality theorem for substitution. (Contributed by NM, 14-May-1993.) | 
| Ref | Expression | 
|---|---|
| sbequ12 | ⊢ (𝑥 = 𝑦 → (𝜑 ↔ [𝑦 / 𝑥]𝜑)) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | sbequ1 2248 | . 2 ⊢ (𝑥 = 𝑦 → (𝜑 → [𝑦 / 𝑥]𝜑)) | |
| 2 | sbequ2 2249 | . 2 ⊢ (𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 → 𝜑)) | |
| 3 | 1, 2 | impbid 212 | 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: sbequ12r 2252 sbequ12a 2254 sb8fOLD 2357 sb8ef 2358 sbbib 2364 axc16ALT 2494 nfsb4t 2504 sbco2 2516 sb8 2522 sb8e 2523 sbal1 2533 sbal2 2534 sbab 2889 cbvrexsvw 3318 cbvralsvwOLD 3319 cbvralsvwOLDOLD 3320 cbvrexsvwOLD 3321 cbvralf 3360 cbvralsv 3366 cbvrexsv 3367 cbvrabwOLD 3474 cbvrab 3479 sbhypfOLD 3545 mob2 3721 reu2 3731 reu6 3732 sbcralt 3872 sbcreu 3876 cbvrabcsfw 3940 cbvreucsf 3943 cbvrabcsf 3944 csbif 4583 cbvopab1 5217 cbvopab1g 5218 cbvopab1s 5220 cbvmptf 5251 cbvmptfg 5252 csbopab 5560 csbopabgALT 5561 opeliunxp 5752 opeliun2xp 5753 ralxpf 5857 cbviotaw 6521 cbviota 6523 csbiota 6554 f1ossf1o 7148 cbvriotaw 7397 cbvriota 7401 csbriota 7403 onminex 7822 tfis 7876 findes 7922 abrexex2g 7989 opabex3d 7990 opabex3rd 7991 opabex3 7992 dfoprab4f 8081 uzind4s 12950 ac6sf2 32634 esumcvg 34087 wl-sb8t 37553 wl-sbalnae 37563 wl-ax11-lem8 37593 sbcrexgOLD 42796 scottabes 44261 pm13.193 44430 2reu8i 47125 ichnfimlem 47450 | 
| Copyright terms: Public domain | W3C validator |