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 1843 | . 2 ⊢ Ⅎ𝑥𝜑 | |
2 | sbcbidv.1 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
3 | 1, 2 | sbcbid 3489 | 1 ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ [𝐴 / 𝑥]𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 [wsbc 3435 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-sbc 3436 |
This theorem is referenced by: sbcbii 3491 opelopabsb 4985 opelopabgf 4995 opelopabf 5000 sbcfng 6042 sbcfg 6043 fmptsnd 6435 wrd2ind 13477 islmod 18867 elmptrab 21630 f1od2 29499 isomnd 29701 isorng 29799 indexa 33528 sdclem2 33538 sdclem1 33539 fdc 33541 sbcalf 33917 sbcexf 33918 hdmap1ffval 37085 hdmap1fval 37086 hdmapffval 37118 hdmapfval 37119 hgmapffval 37177 hgmapfval 37178 rexrabdioph 37358 rexfrabdioph 37359 2rexfrabdioph 37360 3rexfrabdioph 37361 4rexfrabdioph 37362 6rexfrabdioph 37363 7rexfrabdioph 37364 2sbc6g 38616 2sbc5g 38617 |
Copyright terms: Public domain | W3C validator |