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 3457 | . 2 ⊢ (⊤ → ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓)) |
4 | 3 | trud 1484 | 1 ⊢ ([𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 195 ⊤wtru 1476 [wsbc 3402 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-sbc 3403 |
This theorem is referenced by: eqsbc3r 3459 eqsbc3rOLD 3460 sbc3an 3461 sbccomlem 3475 sbccom 3476 sbcrext 3478 sbcrextOLD 3479 sbcabel 3483 csbco 3509 sbcnel12g 3937 sbcne12 3938 csbcom 3946 csbnestgf 3948 sbccsb 3956 sbccsb2 3957 csbab 3960 sbcssg 4035 sbcrel 5128 difopab 5175 sbcfung 5827 tfinds2 6955 mpt2xopovel 7233 f1od2 28887 bnj62 30040 bnj89 30041 bnj156 30050 bnj524 30060 bnj538OLD 30064 bnj610 30071 bnj919 30091 bnj976 30102 bnj110 30182 bnj91 30185 bnj92 30186 bnj106 30192 bnj121 30194 bnj124 30195 bnj125 30196 bnj126 30197 bnj130 30198 bnj154 30202 bnj155 30203 bnj153 30204 bnj207 30205 bnj523 30211 bnj526 30212 bnj539 30215 bnj540 30216 bnj581 30232 bnj591 30235 bnj609 30241 bnj611 30242 bnj934 30259 bnj1000 30265 bnj984 30276 bnj985 30277 bnj1040 30294 bnj1123 30308 bnj1452 30374 bnj1463 30377 sbcalf 33087 sbcexf 33088 sbccom2lem 33099 sbccom2 33100 sbccom2f 33101 sbccom2fi 33102 csbcom2fi 33104 2sbcrex 36366 2sbcrexOLD 36368 sbcrot3 36373 sbcrot5 36374 2rexfrabdioph 36378 3rexfrabdioph 36379 4rexfrabdioph 36380 6rexfrabdioph 36381 7rexfrabdioph 36382 rmydioph 36599 expdiophlem2 36607 sbcheg 37093 sbc3or 37759 sbcbiiOLD 37762 trsbc 37771 onfrALTlem5 37778 csbabgOLD 38072 |
Copyright terms: Public domain | W3C validator |