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 2175. (Revised by Gino Giotto, 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 3701 | 1 ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ [𝐴 / 𝑥]𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 [wsbc 3694 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-ext 2708 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1788 df-sb 2071 df-clab 2715 df-cleq 2729 df-clel 2816 df-sbc 3695 |
This theorem is referenced by: sbcbii 3755 csbied 3849 2nreu 4356 opelopabsb 5411 opelopabgf 5421 opelopabf 5426 sbcfng 6542 sbcfg 6543 fmptsnd 6984 wrd2ind 14288 islmod 19903 elmptrab 22724 f1od2 30776 isomnd 31046 isorng 31217 frpoins3xpg 33524 frpoins3xp3g 33525 indexa 35628 sdclem2 35637 sdclem1 35638 fdc 35640 sbcalf 36009 sbcexf 36010 hdmap1ffval 39546 hdmap1fval 39547 hdmapffval 39577 hdmapfval 39578 hgmapffval 39636 hgmapfval 39637 rexrabdioph 40319 rexfrabdioph 40320 2rexfrabdioph 40321 3rexfrabdioph 40322 4rexfrabdioph 40323 6rexfrabdioph 40324 7rexfrabdioph 40325 2sbc6g 41706 2sbc5g 41707 or2expropbilem1 44198 |
Copyright terms: Public domain | W3C validator |