Metamath Proof Explorer

Theorem uhgr0v0e

Description: The null graph, with no vertices, has no edges. (Contributed by AV, 21-Oct-2020)

Ref Expression
Hypotheses uhgr0v0e.v ⊢V=Vtx⁡G
uhgr0v0e.e ⊢E=Edg⁡G
Assertion uhgr0v0e ⊢G∈UHGraph∧V=∅→E=∅

Proof

Step Hyp Ref Expression
1 uhgr0v0e.v ⊢V=Vtx⁡G
2 uhgr0v0e.e ⊢E=Edg⁡G
3 1 eqeq1i ⊢V=∅↔Vtx⁡G=∅
4 uhgr0vb ⊢G∈UHGraph∧Vtx⁡G=∅→G∈UHGraph↔iEdg⁡G=∅
5 4 biimpd ⊢G∈UHGraph∧Vtx⁡G=∅→G∈UHGraph→iEdg⁡G=∅
6 5 ex ⊢G∈UHGraph→Vtx⁡G=∅→G∈UHGraph→iEdg⁡G=∅
7 3 6 biimtrid ⊢G∈UHGraph→V=∅→G∈UHGraph→iEdg⁡G=∅
8 7 pm2.43a ⊢G∈UHGraph→V=∅→iEdg⁡G=∅
9 8 imp ⊢G∈UHGraph∧V=∅→iEdg⁡G=∅
10 2 eqeq1i ⊢E=∅↔Edg⁡G=∅
11 uhgriedg0edg0 ⊢G∈UHGraph→Edg⁡G=∅↔iEdg⁡G=∅
12 10 11 bitrid ⊢G∈UHGraph→E=∅↔iEdg⁡G=∅
13 12 adantr ⊢G∈UHGraph∧V=∅→E=∅↔iEdg⁡G=∅
14 9 13 mpbird ⊢G∈UHGraph∧V=∅→E=∅