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 2506 with a disjoint variable condition, not requiring ax-13 2372. See sbievw 2095 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 2137 and shorten proof. (Revised by BJ, 18-Jul-2023.) |
Ref | Expression |
---|---|
sbiev.1 | ⊢ Ⅎ𝑥𝜓 |
sbiev.2 | ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
sbiev | ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sb6 2088 | . 2 ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑)) | |
2 | sbiev.1 | . . 3 ⊢ Ⅎ𝑥𝜓 | |
3 | sbiev.2 | . . 3 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
4 | 2, 3 | equsalv 2259 | . 2 ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓) |
5 | 1, 4 | bitri 274 | 1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∀wal 1537 Ⅎwnf 1786 [wsb 2067 |
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 1913 ax-6 1971 ax-7 2011 ax-12 2171 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ex 1783 df-nf 1787 df-sb 2068 |
This theorem is referenced by: sbiedw 2310 sbco2v 2327 mo4f 2567 cbvmowOLD 2604 cbveuwOLD 2608 cbvabwOLD 2813 cbvralfwOLD 3369 cbvreuwOLD 3377 cbvrabw 3424 reu2 3660 rmo4f 3670 sbcralt 3805 sbcreu 3809 sbcel12 4342 sbceqg 4343 sbcbr123 5128 cbvmptf 5183 frpoins2fg 6247 wfis2fgOLD 6260 tfis2f 7702 tfinds 7706 frins2f 9511 clwwlknonclwlknonf1o 28726 dlwwlknondlwlknonf1o 28729 funcnv4mpt 31006 nn0min 31134 ballotlemodife 32464 bnj1321 33007 setinds2f 33755 bj-sbeqALT 35085 scottabf 41858 |
Copyright terms: Public domain | W3C validator |