![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sbcbidv | Structured version Visualization version GIF version |
Description: Formula-building deduction for class substitution. (Contributed by NM, 29-Dec-2014.) Drop ax-12 2167. (Revised by GG, 1-Dec-2023.) |
Ref | Expression |
---|---|
sbcbidv.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
sbcbidv | ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ [𝐴 / 𝑥]𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqidd 2727 | . 2 ⊢ (𝜑 → 𝐴 = 𝐴) | |
2 | sbcbidv.1 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
3 | 1, 2 | sbceqbid 3783 | 1 ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ [𝐴 / 𝑥]𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 [wsbc 3776 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-sbc 3777 |
This theorem is referenced by: sbcbii 3837 csbied 3930 2nreu 4446 opelopabsb 5536 opelopabgf 5546 opelopabf 5551 sbcfng 6725 sbcfg 6726 fmptsnd 7183 frpoins3xpg 8154 frpoins3xp3g 8155 wrd2ind 14731 islmod 20840 elmptrab 23822 f1od2 32635 isomnd 32936 isorng 33177 indexa 37434 sdclem2 37443 sdclem1 37444 fdc 37446 sbcalf 37815 sbcexf 37816 hdmap1ffval 41494 hdmap1fval 41495 hdmapffval 41525 hdmapfval 41526 hgmapffval 41584 hgmapfval 41585 f1o2d2 41957 rexrabdioph 42451 rexfrabdioph 42452 2rexfrabdioph 42453 3rexfrabdioph 42454 4rexfrabdioph 42455 6rexfrabdioph 42456 7rexfrabdioph 42457 2sbc6g 44089 2sbc5g 44090 or2expropbilem1 46647 |
Copyright terms: Public domain | W3C validator |