Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > csbeq2dv | Structured version Visualization version GIF version |
Description: Formula-building deduction rule for class substitution. (Contributed by NM, 10-Nov-2005.) (Revised by Mario Carneiro, 1-Sep-2015.) |
Ref | Expression |
---|---|
csbeq2dv.1 | ⊢ (𝜑 → 𝐵 = 𝐶) |
Ref | Expression |
---|---|
csbeq2dv | ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1830 | . 2 ⊢ Ⅎ𝑥𝜑 | |
2 | csbeq2dv.1 | . 2 ⊢ (𝜑 → 𝐵 = 𝐶) | |
3 | 1, 2 | csbeq2d 3943 | 1 ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1475 ⦋csb 3499 |
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 df-csb 3500 |
This theorem is referenced by: csbeq2i 3945 mpt2mptsx 7122 dmmpt2ssx 7124 fmpt2x 7125 el2mpt2csbcl 7137 offval22 7140 ovmptss 7145 fmpt2co 7147 mpt2sn 7155 mpt2curryd 7282 fvmpt2curryd 7284 cantnffval 8443 fsumcom2 14347 fsumcom2OLD 14348 fprodcom2 14553 fprodcom2OLD 14554 bpolylem 14618 bpolyval 14619 ruclem1 14799 natfval 16429 fucval 16441 evlfval 16680 mpfrcl 19339 pmatcollpw3lem 20407 fsumcn 22481 fsum2cn 22482 dvmptfsum 23542 ttgval 25555 nbgraopALT 25953 msrfval 30688 poimirlem5 32584 poimirlem6 32585 poimirlem7 32586 poimirlem8 32587 poimirlem10 32589 poimirlem11 32590 poimirlem12 32591 poimirlem15 32594 poimirlem16 32595 poimirlem17 32596 poimirlem18 32597 poimirlem19 32598 poimirlem20 32599 poimirlem21 32600 poimirlem22 32601 poimirlem24 32603 poimirlem26 32605 poimirlem27 32606 cdleme31sde 34691 cdlemeg47rv2 34816 rnghmval 41681 dmmpt2ssx2 41908 |
Copyright terms: Public domain | W3C validator |