![]() |
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 2501 with a disjoint variable condition, not requiring ax-13 2371. 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 2258 | . 2 ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓) |
5 | 1, 4 | bitri 274 | 1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∀wal 1539 Ⅎwnf 1785 [wsb 2067 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 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 1782 df-nf 1786 df-sb 2068 |
This theorem is referenced by: sbiedw 2309 sbco2v 2326 mo4f 2561 cbvmowOLD 2598 cbveuwOLD 2602 cbvabwOLD 2807 cbvralfwOLD 3320 cbvreuwOLD 3412 cbvrabw 3467 reu2 3718 rmo4f 3728 sbcralt 3863 sbcreu 3867 sbcel12 4405 sbceqg 4406 sbcbr123 5196 cbvmptf 5251 frpoins2fg 6335 wfis2fgOLD 6348 tfis2f 7829 tfinds 7833 frins2f 9732 clwwlknonclwlknonf1o 29544 dlwwlknondlwlknonf1o 29547 funcnv4mpt 31827 nn0min 31961 ballotlemodife 33391 bnj1321 33933 setinds2f 34645 bj-sbeqALT 35648 scottabf 42834 |
Copyright terms: Public domain | W3C validator |