![]() |
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 3834 | 1 ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1538 ⦋csb 3828 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-12 2175 ax-ext 2770 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1782 df-nf 1786 df-sb 2070 df-clab 2777 df-cleq 2791 df-clel 2870 df-sbc 3721 df-csb 3829 |
This theorem is referenced by: csbeq2i 3836 csbeq12dv 3837 mpomptsx 7744 dmmpossx 7746 fmpox 7747 el2mpocsbcl 7763 offval22 7766 ovmptss 7771 fmpoco 7773 mposn 7781 mpocurryd 7918 fvmpocurryd 7920 cantnffval 9110 fsumcom2 15121 fprodcom2 15330 bpolylem 15394 bpolyval 15395 ruclem1 15576 natfval 17208 fucval 17220 evlfval 17459 mpfrcl 20757 selvffval 20788 selvfval 20789 selvval 20790 pmatcollpw3lem 21388 fsumcn 23475 fsum2cn 23476 dvmptfsum 24578 ttgval 26669 msrfval 32897 poimirlem5 35062 poimirlem6 35063 poimirlem7 35064 poimirlem8 35065 poimirlem10 35067 poimirlem11 35068 poimirlem12 35069 poimirlem15 35072 poimirlem16 35073 poimirlem17 35074 poimirlem18 35075 poimirlem19 35076 poimirlem20 35077 poimirlem21 35078 poimirlem22 35079 poimirlem24 35081 poimirlem26 35083 poimirlem27 35084 cdleme31sde 37681 cdlemeg47rv2 37806 rnghmval 44515 dmmpossx2 44738 |
Copyright terms: Public domain | W3C validator |