![]() |
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 1890 | . 2 ⊢ Ⅎ𝑥𝜑 | |
2 | sbcbidv.1 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
3 | 1, 2 | sbcbid 3750 | 1 ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ [𝐴 / 𝑥]𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 [wsbc 3701 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1775 ax-4 1789 ax-5 1886 ax-6 1945 ax-7 1990 ax-8 2081 ax-9 2089 ax-12 2139 ax-ext 2767 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1760 df-nf 1764 df-sb 2041 df-clab 2774 df-cleq 2786 df-clel 2861 df-sbc 3702 |
This theorem is referenced by: sbcbii 3752 2nreu 4301 opelopabsb 5299 opelopabgf 5309 opelopabf 5314 sbcfng 6371 sbcfg 6372 fmptsnd 6785 wrd2ind 13909 islmod 19316 elmptrab 22107 f1od2 30118 isomnd 30332 isorng 30481 indexa 34486 sdclem2 34495 sdclem1 34496 fdc 34498 sbcalf 34872 sbcexf 34873 hdmap1ffval 38412 hdmap1fval 38413 hdmapffval 38443 hdmapfval 38444 hgmapffval 38502 hgmapfval 38503 rexrabdioph 38827 rexfrabdioph 38828 2rexfrabdioph 38829 3rexfrabdioph 38830 4rexfrabdioph 38831 6rexfrabdioph 38832 7rexfrabdioph 38833 2sbc6g 40237 2sbc5g 40238 or2expropbilem1 42737 |
Copyright terms: Public domain | W3C validator |