![]() |
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.) |
Ref | Expression |
---|---|
sbcbidv.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
sbcbidv | ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ [𝐴 / 𝑥]𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 2010 | . 2 ⊢ Ⅎ𝑥𝜑 | |
2 | sbcbidv.1 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
3 | 1, 2 | sbcbid 3687 | 1 ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ [𝐴 / 𝑥]𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 [wsbc 3633 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-ext 2777 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-clab 2786 df-cleq 2792 df-clel 2795 df-sbc 3634 |
This theorem is referenced by: sbcbii 3689 opelopabsb 5181 opelopabgf 5191 opelopabf 5196 sbcfng 6253 sbcfg 6254 fmptsnd 6664 wrd2ind 13778 wrd2indOLD 13779 islmod 19185 elmptrab 21959 f1od2 30017 isomnd 30217 isorng 30315 indexa 34016 sdclem2 34025 sdclem1 34026 fdc 34028 sbcalf 34404 sbcexf 34405 hdmap1ffval 37816 hdmap1fval 37817 hdmapffval 37847 hdmapfval 37848 hgmapffval 37906 hgmapfval 37907 rexrabdioph 38144 rexfrabdioph 38145 2rexfrabdioph 38146 3rexfrabdioph 38147 4rexfrabdioph 38148 6rexfrabdioph 38149 7rexfrabdioph 38150 2sbc6g 39397 2sbc5g 39398 |
Copyright terms: Public domain | W3C validator |