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

Theorem iscusgra 23515
 Description: The property of being a complete (undirected simple) graph. (Contributed by Alexander van der Vekens, 12-Oct-2017.)
Assertion
Ref Expression
iscusgra ComplUSGrph USGrph
Distinct variable groups:   ,,   ,,
Allowed substitution hints:   (,)   (,)

Proof of Theorem iscusgra
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 breq12 4404 . . 3 USGrph USGrph
2 simpl 457 . . . 4
3 difeq1 3574 . . . . . 6
43adantr 465 . . . . 5
5 rneq 5172 . . . . . . 7
65adantl 466 . . . . . 6
76eleq2d 2524 . . . . 5
84, 7raleqbidv 3035 . . . 4
92, 8raleqbidv 3035 . . 3
101, 9anbi12d 710 . 2 USGrph USGrph
11 df-cusgra 23484 . 2 ComplUSGrph USGrph
1210, 11brabga 4710 1 ComplUSGrph USGrph
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 184   wa 369   wceq 1370   wcel 1758  wral 2798   cdif 3432  csn 3984  cpr 3986   class class class wbr 4399   crn 4948   USGrph cusg 23415   ComplUSGrph ccusgra 23481 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4520  ax-nul 4528  ax-pr 4638 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2649  df-ral 2803  df-rab 2807  df-v 3078  df-dif 3438  df-un 3440  df-in 3442  df-ss 3449  df-nul 3745  df-if 3899  df-sn 3985  df-pr 3987  df-op 3991  df-br 4400  df-opab 4458  df-cnv 4955  df-dm 4957  df-rn 4958  df-cusgra 23484 This theorem is referenced by:  iscusgra0  23516  cusgra0v  23519  cusgra1v  23520  cusgra2v  23521  nbcusgra  23522  cusgra3v  23523  cusgraexi  23527  cusgrares  23531  cusgrauvtxb  23555  cusconngra  23713
 Copyright terms: Public domain W3C validator