Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > csbeq2dv | Structured version Visualization version GIF version |
Description: Formula-building deduction 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 1915 | . 2 ⊢ Ⅎ𝑥𝜑 | |
2 | csbeq2dv.1 | . 2 ⊢ (𝜑 → 𝐵 = 𝐶) | |
3 | 1, 2 | csbeq2d 3889 | 1 ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1537 ⦋csb 3883 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-12 2177 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-ex 1781 df-nf 1785 df-sb 2070 df-clab 2800 df-cleq 2814 df-clel 2893 df-sbc 3773 df-csb 3884 |
This theorem is referenced by: csbeq2i 3891 csbeq12dv 3892 mpomptsx 7762 dmmpossx 7764 fmpox 7765 el2mpocsbcl 7780 offval22 7783 ovmptss 7788 fmpoco 7790 mposn 7798 mpocurryd 7935 fvmpocurryd 7937 cantnffval 9126 fsumcom2 15129 fprodcom2 15338 bpolylem 15402 bpolyval 15403 ruclem1 15584 natfval 17216 fucval 17228 evlfval 17467 mpfrcl 20298 selvffval 20329 selvfval 20330 selvval 20331 pmatcollpw3lem 21391 fsumcn 23478 fsum2cn 23479 dvmptfsum 24572 ttgval 26661 msrfval 32784 poimirlem5 34912 poimirlem6 34913 poimirlem7 34914 poimirlem8 34915 poimirlem10 34917 poimirlem11 34918 poimirlem12 34919 poimirlem15 34922 poimirlem16 34923 poimirlem17 34924 poimirlem18 34925 poimirlem19 34926 poimirlem20 34927 poimirlem21 34928 poimirlem22 34929 poimirlem24 34931 poimirlem26 34933 poimirlem27 34934 cdleme31sde 37536 cdlemeg47rv2 37661 rnghmval 44182 dmmpossx2 44405 |
Copyright terms: Public domain | W3C validator |