![]() |
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 2505 with a disjoint variable condition, not requiring ax-13 2371. See sbievw 2096 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 2138 and shorten proof. (Revised by BJ, 18-Jul-2023.) |
Ref | Expression |
---|---|
sbiev.1 | ⊢ Ⅎ𝑥𝜓 |
sbiev.2 | ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
sbiev | ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sb6 2089 | . 2 ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑)) | |
2 | sbiev.1 | . . 3 ⊢ Ⅎ𝑥𝜓 | |
3 | sbiev.2 | . . 3 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
4 | 2, 3 | equsalv 2259 | . 2 ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓) |
5 | 1, 4 | bitri 275 | 1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∀wal 1540 Ⅎwnf 1786 [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-nf 1787 df-sb 2069 |
This theorem is referenced by: sbiedw 2310 sbco2v 2327 mo4f 2566 cbvmowOLD 2603 cbveuwOLD 2607 cbvabwOLD 2812 cbvralfwOLD 3307 cbvreuwOLD 3392 cbvrabw 3442 reu2 3688 rmo4f 3698 sbcralt 3833 sbcreu 3837 sbcel12 4373 sbceqg 4374 sbcbr123 5164 cbvmptf 5219 frpoins2fg 6303 wfis2fgOLD 6316 tfis2f 7797 tfinds 7801 frins2f 9696 clwwlknonclwlknonf1o 29348 dlwwlknondlwlknonf1o 29351 funcnv4mpt 31627 nn0min 31758 ballotlemodife 33137 bnj1321 33679 setinds2f 34393 bj-sbeqALT 35396 scottabf 42594 |
Copyright terms: Public domain | W3C validator |