Mathbox for Mario Carneiro < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  mdvval Structured version   Unicode version

Theorem mdvval 28842
 Description: The set of disjoint variable conditions, which are pairs of distinct variables. (This definition differs from appendix C, which uses unordered pairs instead. We use ordered pairs, but all sets of DV conditions of interest will be symmetric, so it does not matter.) (Contributed by Mario Carneiro, 18-Jul-2016.)
Hypotheses
Ref Expression
mdvval.v mVR
mdvval.d mDV
Assertion
Ref Expression
mdvval

Proof of Theorem mdvval
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 mdvval.d . 2 mDV
2 fveq2 5856 . . . . . . 7 mVR mVR
3 mdvval.v . . . . . . 7 mVR
42, 3syl6eqr 2502 . . . . . 6 mVR
54sqxpeqd 5015 . . . . 5 mVR mVR
65difeq1d 3606 . . . 4 mVR mVR
7 df-mdv 28826 . . . 4 mDV mVR mVR
8 fvex 5866 . . . . . 6 mVR
98, 8xpex 6589 . . . . 5 mVR mVR
10 difexg 4585 . . . . 5 mVR mVR mVR mVR
119, 10ax-mp 5 . . . 4 mVR mVR
126, 7, 11fvmpt3i 5945 . . 3 mDV
13 0dif 3885 . . . . 5
1413eqcomi 2456 . . . 4
15 fvprc 5850 . . . 4 mDV
16 fvprc 5850 . . . . . . . 8 mVR
173, 16syl5eq 2496 . . . . . . 7
1817xpeq2d 5013 . . . . . 6
19 xp0 5415 . . . . . 6
2018, 19syl6eq 2500 . . . . 5
2120difeq1d 3606 . . . 4
2214, 15, 213eqtr4a 2510 . . 3 mDV
2312, 22pm2.61i 164 . 2 mDV
241, 23eqtri 2472 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wceq 1383   wcel 1804  cvv 3095   cdif 3458  c0 3770   cid 4780   cxp 4987  cfv 5578  mVRcmvar 28799  mDVcmdv 28806 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pow 4615  ax-pr 4676  ax-un 6577 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-ral 2798  df-rex 2799  df-rab 2802  df-v 3097  df-sbc 3314  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-pw 3999  df-sn 4015  df-pr 4017  df-op 4021  df-uni 4235  df-br 4438  df-opab 4496  df-mpt 4497  df-id 4785  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-iota 5541  df-fun 5580  df-fv 5586  df-mdv 28826 This theorem is referenced by:  mthmpps  28920  mclsppslem  28921
 Copyright terms: Public domain W3C validator