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 2537 with a disjoint variable condition, not requiring ax-13 2381. See sbievw 2094 for a version with a disjoint variable condition requiring fewer axioms. (Contributed by Wolf Lammen, 18-Jan-2023.) Remove dependence on ax-10 2136 and shorten proof. (Revised by BJ, 18-Jul-2023.) |
Ref | Expression |
---|---|
sbiev.1 | ⊢ Ⅎ𝑥𝜓 |
sbiev.2 | ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
sbiev | ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sb6 2084 | . 2 ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑)) | |
2 | sbiev.1 | . . 3 ⊢ Ⅎ𝑥𝜓 | |
3 | sbiev.2 | . . 3 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
4 | 2, 3 | equsalv 2258 | . 2 ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓) |
5 | 1, 4 | bitri 276 | 1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∀wal 1526 Ⅎwnf 1775 [wsb 2060 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-12 2167 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-nf 1776 df-sb 2061 |
This theorem is referenced by: sbiedw 2323 sbiedwOLD 2324 sbco2v 2343 mo4f 2644 cbvmow 2681 cbveuw 2683 cbvabw 2887 cbvralfw 3435 cbvreuw 3441 cbvrabw 3487 reu2 3713 rmo4f 3723 sbcralt 3852 sbcreu 3856 sbcel12 4357 sbceqg 4358 sbcbr123 5111 cbvmptf 5156 wfis2fg 6178 tfis2f 7559 tfinds 7563 clwwlknonclwlknonf1o 28068 dlwwlknondlwlknonf1o 28071 funcnv4mpt 30342 nn0min 30463 ballotlemodife 31654 setinds2f 32921 frpoins2fg 32979 frins2fg 32986 scottabf 40453 |
Copyright terms: Public domain | W3C validator |