Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > sbcbii | Structured version Visualization version GIF version |
Description: Formula-building inference for class substitution. (Contributed by NM, 11-Nov-2005.) |
Ref | Expression |
---|---|
sbcbii.1 | ⊢ (𝜑 ↔ 𝜓) |
Ref | Expression |
---|---|
sbcbii | ⊢ ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sbcbii.1 | . . . 4 ⊢ (𝜑 ↔ 𝜓) | |
2 | 1 | a1i 11 | . . 3 ⊢ (⊤ → (𝜑 ↔ 𝜓)) |
3 | 2 | sbcbidv 3824 | . 2 ⊢ (⊤ → ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓)) |
4 | 3 | mptru 1535 | 1 ⊢ ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 207 ⊤wtru 1529 [wsbc 3769 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-tru 1531 df-ex 1772 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-sbc 3770 |
This theorem is referenced by: eqsbc3r 3834 sbc3an 3835 sbccomlem 3850 sbccom 3851 sbcrext 3853 sbcabel 3858 csbcow 3895 csbco 3896 sbcnel12g 4360 sbcne12 4361 csbcom 4366 csbnestgfw 4368 csbnestgf 4373 sbccsb 4382 sbccsb2 4383 csbab 4386 2nreu 4389 sbcssg 4459 sbcop 5371 sbcrel 5648 difopab 5695 sbcfung 6372 tfinds2 7567 mpoxopovel 7875 f1od2 30383 bnj62 31889 bnj89 31890 bnj156 31897 bnj524 31907 bnj610 31917 bnj919 31937 bnj976 31948 bnj110 32029 bnj91 32032 bnj92 32033 bnj106 32039 bnj121 32041 bnj124 32042 bnj125 32043 bnj126 32044 bnj130 32045 bnj154 32049 bnj155 32050 bnj153 32051 bnj207 32052 bnj523 32058 bnj526 32059 bnj539 32062 bnj540 32063 bnj581 32079 bnj591 32082 bnj609 32088 bnj611 32089 bnj934 32106 bnj1000 32112 bnj984 32123 bnj985 32124 bnj1040 32141 bnj1123 32155 bnj1452 32221 bnj1463 32224 sbcalf 35273 sbcexf 35274 sbccom2lem 35283 sbccom2 35284 sbccom2f 35285 sbccom2fi 35286 csbcom2fi 35287 2sbcrex 39259 2sbcrexOLD 39261 sbcrot3 39266 sbcrot5 39267 2rexfrabdioph 39271 3rexfrabdioph 39272 4rexfrabdioph 39273 6rexfrabdioph 39274 7rexfrabdioph 39275 rmydioph 39489 expdiophlem2 39497 sbcheg 40003 sbc3or 40743 trsbc 40751 onfrALTlem5 40753 eqsbc3rVD 41051 sbcoreleleqVD 41070 onfrALTlem5VD 41096 ich2exprop 43510 |
Copyright terms: Public domain | W3C validator |