![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sbcbii | Structured version Visualization version GIF version |
Description: Formula-building inference rule 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 3523 | . 2 ⊢ (⊤ → ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓)) |
4 | 3 | trud 1533 | 1 ⊢ ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 ⊤wtru 1524 [wsbc 3468 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-sbc 3469 |
This theorem is referenced by: eqsbc3r 3525 eqsbc3rOLD 3526 sbc3an 3527 sbccomlem 3541 sbccom 3542 sbcrext 3544 sbcrextOLD 3545 sbcabel 3550 csbco 3576 sbcnel12g 4018 sbcne12 4019 csbcom 4027 csbnestgf 4029 sbccsb 4037 sbccsb2 4038 csbab 4041 sbcssg 4118 sbcrel 5239 difopab 5286 sbcfung 5950 tfinds2 7105 mpt2xopovel 7391 f1od2 29627 bnj62 30914 bnj89 30915 bnj156 30922 bnj524 30932 bnj538OLD 30936 bnj610 30943 bnj919 30963 bnj976 30974 bnj110 31054 bnj91 31057 bnj92 31058 bnj106 31064 bnj121 31066 bnj124 31067 bnj125 31068 bnj126 31069 bnj130 31070 bnj154 31074 bnj155 31075 bnj153 31076 bnj207 31077 bnj523 31083 bnj526 31084 bnj539 31087 bnj540 31088 bnj581 31104 bnj591 31107 bnj609 31113 bnj611 31114 bnj934 31131 bnj1000 31137 bnj984 31148 bnj985 31149 bnj1040 31166 bnj1123 31180 bnj1452 31246 bnj1463 31249 sbcalf 34047 sbcexf 34048 sbccom2lem 34059 sbccom2 34060 sbccom2f 34061 sbccom2fi 34062 csbcom2fi 34064 2sbcrex 37665 2sbcrexOLD 37667 sbcrot3 37672 sbcrot5 37673 2rexfrabdioph 37677 3rexfrabdioph 37678 4rexfrabdioph 37679 6rexfrabdioph 37680 7rexfrabdioph 37681 rmydioph 37898 expdiophlem2 37906 sbcheg 38390 sbc3or 39055 sbcbiiOLD 39058 sbc3orgOLD 39059 trsbc 39067 sbcssOLD 39073 onfrALTlem5 39074 csbabgOLD 39367 onfrALTlem5VD 39435 |
Copyright terms: Public domain | W3C validator |