Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > sbcbidv | Structured version Visualization version GIF version |
Description: Formula-building deduction rule for class substitution. (Contributed by NM, 29-Dec-2014.) |
Ref | Expression |
---|---|
sbcbidv.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
sbcbidv | ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ [𝐴 / 𝑥]𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1830 | . 2 ⊢ Ⅎ𝑥𝜑 | |
2 | sbcbidv.1 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
3 | 1, 2 | sbcbid 3456 | 1 ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ [𝐴 / 𝑥]𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 [wsbc 3402 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-sbc 3403 |
This theorem is referenced by: sbcbii 3458 opelopabsb 4910 opelopabgf 4920 opelopabf 4925 sbcfng 5955 sbcfg 5956 fmptsnd 6340 wrd2ind 13329 islmod 18690 elmptrab 21440 nbgraopALT 25953 f1od2 28887 isomnd 29032 isorng 29130 indexa 32698 sdclem2 32708 sdclem1 32709 fdc 32711 sbcalf 33087 sbcexf 33088 hdmap1ffval 36103 hdmap1fval 36104 hdmapffval 36136 hdmapfval 36137 hgmapffval 36195 hgmapfval 36196 rexrabdioph 36376 rexfrabdioph 36377 2rexfrabdioph 36378 3rexfrabdioph 36379 4rexfrabdioph 36380 6rexfrabdioph 36381 7rexfrabdioph 36382 2sbc6g 37638 2sbc5g 37639 |
Copyright terms: Public domain | W3C validator |