Theorem usgrav 25867

Description: The classes of vertices and edges of an undirected simple graph without loops are sets. (Contributed by Alexander van der Vekens, 19-Aug-2017.)

Assertion

Ref	Expression
usgrav	⊢ (𝑉 USGrph 𝐸 → (𝑉 ∈ V ∧ 𝐸 ∈ V))

Proof of Theorem usgrav

Step	Hyp	Ref	Expression
1		relusgra 25864	. . 3 ⊢ Rel USGrph
2	1	brrelexi 5082	. 2 ⊢ (𝑉 USGrph 𝐸 → 𝑉 ∈ V)
3	1	brrelex2i 5083	. 2 ⊢ (𝑉 USGrph 𝐸 → 𝐸 ∈ V)
4	2, 3	jca 553	1 ⊢ (𝑉 USGrph 𝐸 → (𝑉 ∈ V ∧ 𝐸 ∈ V))

Syntax hints:   → wi 4   ∧ wa 383   ∈ wcel 1977  Vcvv 3173   class class class wbr 4583   USGrph cusg 25859

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584  df-opab 4644  df-xp 5044  df-rel 5045  df-usgra 25862

This theorem is referenced by:  usgraf  25875  usgraf0  25877  usisuslgra  25894  usgrares  25898  usgra0v  25900  usgra1v  25919  usgraedgleord  25923  fiusgraedgfi  25936  usgrafisindb0  25937  usgrafisindb1  25938  usgrares1  25939  usgrafisinds  25942  usgrafisbase  25943  nbusgra  25957  nbgrasym  25968  nbgraf1olem1  25970  cusgra2v  25991  nbcusgra  25992  cusgra3v  25993  cusgrares  26001  cusgrasize2inds  26005  cusgrafi  26010  sizeusglecusg  26014  uvtxnbgra  26021  cusgrauvtxb  26024  uvtxnb  26025  usgra2adedgspth  26141  usgra2adedgwlk  26142  usgra2adedgwlkon  26143  constr3trl  26187  constr3pth  26188  constr3cycl  26189  cusconngra  26204  clwwlkgt0  26299  clwwlkn0  26302  clwwlkn2  26303  clwlkisclwwlk  26317  hashclwwlkn  26363  clwwlkndivn  26364  clwlkfclwwlk  26371  usg2wlkonot  26410  usg2wotspth  26411  2pthwlkonot  26412  usg2spthonot0  26416  usg2spthonot1  26417  vdusgraval  26434  vdgrnn0pnf  26436  hashnbgravdg  26440  usgravd0nedg  26445  cusgraisrusgra  26465  0eusgraiff0rgra  26466  rusgraprop3  26470  rusgrasn  26472  rusgranumwwlkl1  26473  rusgranumwlkl1  26474  rusgranumwlkb0  26480  rusgra0edg  26482  frgra1v  26525  frgra2v  26526  frgra3v  26529  2pthfrgra  26538  3cyclfrgrarn  26540  frconngra  26548  vdfrgra0  26549  vdgn0frgrav2  26551  vdgn1frgrav2  26553  vdgfrgragt2  26554  frgrawopreglem1  26571  frg2wot1  26584  frghash2spot  26590  usg2spot2nb  26592  usgreg2spot  26594  frgraregorufrg  26599  extwwlkfablem1  26601  extwwlkfablem2  26605  numclwwlkovfel2  26610  numclwwlkovf2ex  26613  numclwwlkovgelim  26616  numclwwlk1  26625  numclwwlkqhash  26627  numclwwlk3lem  26635  numclwwlk3  26636  numclwwlk4  26637  numclwwlk5  26639  numclwwlk6  26640  frgrareg  26644