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 2373. See sbievw 2103 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 2145 and shorten proof. (Revised by BJ, 18-Jul-2023.) |
Ref | Expression |
---|---|
sbiev.1 | ⊢ Ⅎ𝑥𝜓 |
sbiev.2 | ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
sbiev | ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sb6 2095 | . 2 ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑)) | |
2 | sbiev.1 | . . 3 ⊢ Ⅎ𝑥𝜓 | |
3 | sbiev.2 | . . 3 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
4 | 2, 3 | equsalv 2268 | . 2 ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓) |
5 | 1, 4 | bitri 278 | 1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∀wal 1540 Ⅎwnf 1790 [wsb 2074 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-12 2179 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1787 df-nf 1791 df-sb 2075 |
This theorem is referenced by: sbiedw 2318 sbiedwOLD 2319 sbco2v 2335 mo4f 2568 cbvmowOLD 2606 cbveuwOLD 2610 cbvabwOLD 2809 cbvralfwOLD 3337 cbvreuw 3343 cbvrabw 3392 reu2 3625 rmo4f 3635 sbcralt 3764 sbcreu 3768 sbcel12 4299 sbceqg 4300 sbcbr123 5085 cbvmptf 5130 wfis2fg 6167 tfis2f 7592 tfinds 7596 clwwlknonclwlknonf1o 28302 dlwwlknondlwlknonf1o 28305 funcnv4mpt 30584 nn0min 30712 ballotlemodife 32037 bnj1321 32581 setinds2f 33332 frpoins2fg 33390 frins2fg 33400 bj-sbeqALT 34732 scottabf 41423 |
Copyright terms: Public domain | W3C validator |