| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > sbiev | Structured version Visualization version GIF version | ||
| Description: Conversion of implicit substitution to explicit substitution. Version of sbie 2507 with a disjoint variable condition, not requiring ax-13 2377. See sbievw 2093 for a version with a disjoint variable condition requiring fewer axioms. (Contributed by NM, 30-Jun-1994.) (Revised by Wolf Lammen, 18-Jan-2023.) Remove dependence on ax-10 2141 and shorten proof. (Revised by BJ, 18-Jul-2023.) (Proof shortened by SN, 24-Jul-2025.) |
| Ref | Expression |
|---|---|
| sbiev.1 | ⊢ Ⅎ𝑥𝜓 |
| sbiev.2 | ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) |
| Ref | Expression |
|---|---|
| sbiev | ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sbiev.2 | . . 3 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
| 2 | 1 | sbbiiev 2092 | . 2 ⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜓) |
| 3 | sbiev.1 | . . 3 ⊢ Ⅎ𝑥𝜓 | |
| 4 | 3 | sbf 2271 | . 2 ⊢ ([𝑦 / 𝑥]𝜓 ↔ 𝜓) |
| 5 | 2, 4 | bitri 275 | 1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 Ⅎwnf 1783 [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-nf 1784 df-sb 2065 |
| This theorem is referenced by: sbiedw 2316 sbco2v 2332 mo4f 2567 cbvreuwOLD 3415 cbvrabwOLD 3474 reu2 3731 rmo4f 3741 sbcralt 3872 sbcreu 3876 sbcel12 4411 sbceqg 4412 sbcbr123 5197 cbvmptf 5251 frpoins2fg 6365 wfis2fgOLD 6378 tfis2f 7877 tfinds 7881 frins2f 9793 clwwlknonclwlknonf1o 30381 dlwwlknondlwlknonf1o 30384 funcnv4mpt 32679 nn0min 32822 ballotlemodife 34500 bnj1321 35041 setinds2f 35780 bj-sbeqALT 36901 scottabf 44259 |
| Copyright terms: Public domain | W3C validator |