Mathbox for Rodolfo Medina < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  prter2 Unicode version

Theorem prter2 26340
 Description: The quotient set of the equivalence relation generated by a partition equals the partition itself. (Contributed by Rodolfo Medina, 17-Oct-2010.)
Hypothesis
Ref Expression
prtlem18.1
Assertion
Ref Expression
prter2
Distinct variable group:   ,,,
Allowed substitution hints:   (,,)

Proof of Theorem prter2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 rexcom4 2892 . . . . . . . . . . 11
2 r19.41v 2778 . . . . . . . . . . . 12
32exbii 1587 . . . . . . . . . . 11
41, 3bitri 240 . . . . . . . . . 10
5 df-rex 2634 . . . . . . . . . . 11
65rexbii 2653 . . . . . . . . . 10
7 vex 2876 . . . . . . . . . . . 12
87elqs 6854 . . . . . . . . . . 11
9 df-rex 2634 . . . . . . . . . . . 12
10 eluni2 3933 . . . . . . . . . . . . . 14
1110anbi1i 676 . . . . . . . . . . . . 13
1211exbii 1587 . . . . . . . . . . . 12
139, 12bitri 240 . . . . . . . . . . 11
148, 13bitri 240 . . . . . . . . . 10
154, 6, 143bitr4ri 269 . . . . . . . . 9
16 prtlem18.1 . . . . . . . . . . . 12
1716prtlem19 26337 . . . . . . . . . . 11
1817ralrimivv 2719 . . . . . . . . . 10
19 2r19.29 26311 . . . . . . . . . . 11
2019ex 423 . . . . . . . . . 10
2118, 20syl 15 . . . . . . . . 9
2215, 21syl5bi 208 . . . . . . . 8
23 eqtr3 2385 . . . . . . . . . 10
2423reximi 2735 . . . . . . . . 9
2524reximi 2735 . . . . . . . 8
2622, 25syl6 29 . . . . . . 7
27 df-rex 2634 . . . . . . . . . 10
28 19.41v 1911 . . . . . . . . . 10
2927, 28bitri 240 . . . . . . . . 9
3029simprbi 450 . . . . . . . 8
3130reximi 2735 . . . . . . 7
3226, 31syl6 29 . . . . . 6
33 risset 2675 . . . . . 6
3432, 33syl6ibr 218 . . . . 5
3516prtlem400 26329 . . . . . 6
36 prtlem90 26314 . . . . . 6
3735, 36mp1i 11 . . . . 5
3834, 37jcad 519 . . . 4
39 eldifsn 3842 . . . 4
4038, 39syl6ibr 218 . . 3
41 0ex 4252 . . . . . . . 8
42 prtlem80 26315 . . . . . . . 8
4341, 42ax-mp 8 . . . . . . 7
44 n0el 26316 . . . . . . 7
4543, 44mpbi 199 . . . . . 6
4645rspec 2692 . . . . 5
47 eldifi 3385 . . . . 5
4846, 47jca 518 . . . 4
4916prtlem19 26337 . . . . . . . . 9
5049ancomsd 440 . . . . . . . 8
51 elunii 3934 . . . . . . . 8
5250, 51jca2r 26300 . . . . . . 7
53 prtlem11 26325 . . . . . . . . 9
547, 53ax-mp 8 . . . . . . . 8
5554imp 418 . . . . . . 7
5652, 55syl6 29 . . . . . 6
5756eximdv 1627 . . . . 5
58 19.41v 1911 . . . . 5
59 19.9v 1669 . . . . 5
6057, 58, 593imtr3g 260 . . . 4
6148, 60syl5 28 . . 3
6240, 61impbid 183 . 2
6362eqrdv 2364 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wa 358  wex 1546   wceq 1647   wcel 1715   wne 2529  wral 2628  wrex 2629  cvv 2873   cdif 3235  c0 3543  csn 3729  cuni 3929  copab 4178  cec 6800  cqs 6801   wprt 26330 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-14 1719  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347  ax-sep 4243  ax-nul 4251  ax-pr 4316 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 937  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-eu 2221  df-mo 2222  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-ne 2531  df-ral 2633  df-rex 2634  df-rab 2637  df-v 2875  df-sbc 3078  df-dif 3241  df-un 3243  df-in 3245  df-ss 3252  df-nul 3544  df-if 3655  df-sn 3735  df-pr 3736  df-op 3738  df-uni 3930  df-br 4126  df-opab 4180  df-xp 4798  df-cnv 4800  df-dm 4802  df-rn 4803  df-res 4804  df-ima 4805  df-ec 6804  df-qs 6808  df-prt 26331
 Copyright terms: Public domain W3C validator