Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  cusgra2v Structured version   Visualization version   Unicode version

Theorem cusgra2v 25202
 Description: A graph with two (different) vertices is complete if and only if there is an edge between these two vertices. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Proof shortened by Alexander van der Vekens, 16-Dec-2017.)
Assertion
Ref Expression
cusgra2v USGrph ComplUSGrph

Proof of Theorem cusgra2v
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 usgrav 25077 . . . . 5 USGrph
21adantr 467 . . . 4 USGrph
3 iscusgra 25196 . . . 4 ComplUSGrph USGrph
42, 3syl 17 . . 3 USGrph ComplUSGrph USGrph
5 3simpa 1006 . . . . . 6
65adantl 468 . . . . 5 USGrph
7 sneq 3980 . . . . . . . 8
87difeq2d 3553 . . . . . . 7
9 preq2 4055 . . . . . . . 8
109eleq1d 2515 . . . . . . 7
118, 10raleqbidv 3003 . . . . . 6
12 sneq 3980 . . . . . . . 8
1312difeq2d 3553 . . . . . . 7
14 preq2 4055 . . . . . . . 8
1514eleq1d 2515 . . . . . . 7
1613, 15raleqbidv 3003 . . . . . 6
1711, 16ralprg 4023 . . . . 5
186, 17syl 17 . . . 4 USGrph
19 ibar 507 . . . . 5 USGrph USGrph
2019adantr 467 . . . 4 USGrph USGrph
21 difprsn1 4111 . . . . . . . . . 10
22213ad2ant3 1032 . . . . . . . . 9
2322adantl 468 . . . . . . . 8 USGrph
2423raleqdv 2995 . . . . . . 7 USGrph
25 preq1 4054 . . . . . . . . . . 11
2625eleq1d 2515 . . . . . . . . . 10
2726ralsng 4008 . . . . . . . . 9
28273ad2ant2 1031 . . . . . . . 8
2928adantl 468 . . . . . . 7 USGrph
3024, 29bitrd 257 . . . . . 6 USGrph
31 difprsn2 4112 . . . . . . . . . 10
32313ad2ant3 1032 . . . . . . . . 9
3332adantl 468 . . . . . . . 8 USGrph
3433raleqdv 2995 . . . . . . 7 USGrph
35 preq1 4054 . . . . . . . . . . 11
3635eleq1d 2515 . . . . . . . . . 10
3736ralsng 4008 . . . . . . . . 9
38373ad2ant1 1030 . . . . . . . 8
3938adantl 468 . . . . . . 7 USGrph
4034, 39bitrd 257 . . . . . 6 USGrph
4130, 40anbi12d 718 . . . . 5 USGrph
42 prcom 4053 . . . . . . . 8
4342eleq1i 2522 . . . . . . 7
4443anbi1i 702 . . . . . 6
45 anidm 650 . . . . . 6
4644, 45bitri 253 . . . . 5
4741, 46syl6bb 265 . . . 4 USGrph
4818, 20, 473bitr3d 287 . . 3 USGrph USGrph
494, 48bitrd 257 . 2 USGrph ComplUSGrph
5049expcom 437 1 USGrph ComplUSGrph
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 188   wa 371   w3a 986   wceq 1446   wcel 1889   wne 2624  wral 2739  cvv 3047   cdif 3403  csn 3970  cpr 3972   class class class wbr 4405   crn 4838   USGrph cusg 25069   ComplUSGrph ccusgra 25158 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-9 1898  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433  ax-sep 4528  ax-nul 4537  ax-pr 4642 This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 988  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-eu 2305  df-mo 2306  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-ne 2626  df-ral 2744  df-rex 2745  df-rab 2748  df-v 3049  df-sbc 3270  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-nul 3734  df-if 3884  df-sn 3971  df-pr 3973  df-op 3977  df-br 4406  df-opab 4465  df-xp 4843  df-rel 4844  df-cnv 4845  df-dm 4847  df-rn 4848  df-usgra 25072  df-cusgra 25161 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator