![]() |
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 2241 | . 2 ⊢ (𝑥 = 𝑦 → (𝜑 → [𝑦 / 𝑥]𝜑)) | |
2 | sbequ2 2242 | . 2 ⊢ (𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 → 𝜑)) | |
3 | 1, 2 | impbid 211 | 1 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ [𝑦 / 𝑥]𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 [wsb 2068 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-12 2172 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ex 1783 df-sb 2069 |
This theorem is referenced by: sbequ12r 2245 sbequ12a 2247 sb5OLD 2269 sb8fOLD 2351 sb8ef 2352 sbbib 2358 axc16ALT 2489 nfsb4t 2499 sbco2 2511 sb8 2517 sb8e 2518 sbal1 2528 sbal2 2529 clelabOLD 2881 sbab 2883 nfabdwOLD 2928 cbvralsvw 3315 cbvrexsvw 3316 cbvralsvwOLD 3317 cbvrexsvwOLD 3318 cbvralfwOLD 3321 cbvralf 3357 cbvralsv 3363 cbvrexsv 3364 cbvrabw 3468 cbvrab 3474 sbhypfOLD 3539 mob2 3710 reu2 3720 reu6 3721 sbcralt 3865 sbcreu 3869 cbvrabcsfw 3936 cbvreucsf 3939 cbvrabcsf 3940 csbif 4584 cbvopab1 5222 cbvopab1g 5223 cbvopab1s 5225 cbvmptf 5256 cbvmptfg 5257 csbopab 5554 csbopabgALT 5555 opeliunxp 5741 ralxpf 5844 cbviotaw 6499 cbviota 6502 csbiota 6533 f1ossf1o 7121 cbvriotaw 7369 cbvriota 7374 csbriota 7376 onminex 7785 tfis 7839 findes 7888 abrexex2g 7946 opabex3d 7947 opabex3rd 7948 opabex3 7949 dfoprab4f 8037 uzind4s 12888 ac6sf2 31827 esumcvg 33022 wl-sb8t 36355 wl-sbalnae 36365 wl-ax11-lem8 36392 sbcrexgOLD 41456 scottabes 42934 pm13.193 43103 2reu8i 45756 ichnfimlem 46066 opeliun2xp 46910 |
Copyright terms: Public domain | W3C validator |