| 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 2177. (Revised by GG, 1-Dec-2023.) |
| Ref | Expression |
|---|---|
| sbcbidv.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
| Ref | Expression |
|---|---|
| sbcbidv | ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ [𝐴 / 𝑥]𝜒)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eqidd 2738 | . 2 ⊢ (𝜑 → 𝐴 = 𝐴) | |
| 2 | sbcbidv.1 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
| 3 | 1, 2 | sbceqbid 3795 | 1 ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ [𝐴 / 𝑥]𝜒)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 [wsbc 3788 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-sbc 3789 |
| This theorem is referenced by: sbcbii 3846 csbeq2dv 3906 csbied 3935 2nreu 4444 opelopabsb 5535 opelopabgf 5545 opelopabf 5550 sbcfng 6733 sbcfg 6734 fmptsnd 7189 frpoins3xpg 8165 frpoins3xp3g 8166 wrd2ind 14761 islmod 20862 elmptrab 23835 f1od2 32732 isomnd 33078 isorng 33329 indexa 37740 sdclem2 37749 sdclem1 37750 fdc 37752 sbcalf 38121 sbcexf 38122 hdmap1ffval 41797 hdmap1fval 41798 hdmapffval 41828 hdmapfval 41829 hgmapffval 41887 hgmapfval 41888 f1o2d2 42274 rexrabdioph 42805 rexfrabdioph 42806 2rexfrabdioph 42807 3rexfrabdioph 42808 4rexfrabdioph 42809 6rexfrabdioph 42810 7rexfrabdioph 42811 2sbc6g 44434 2sbc5g 44435 or2expropbilem1 47044 |
| Copyright terms: Public domain | W3C validator |