Step |
Hyp |
Ref |
Expression |
1 |
|
f10 |
⊢ ∅ : ∅ –1-1→ { 𝑥 ∈ ( 𝒫 ∅ ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } |
2 |
|
dm0 |
⊢ dom ∅ = ∅ |
3 |
|
f1eq2 |
⊢ ( dom ∅ = ∅ → ( ∅ : dom ∅ –1-1→ { 𝑥 ∈ ( 𝒫 ∅ ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ↔ ∅ : ∅ –1-1→ { 𝑥 ∈ ( 𝒫 ∅ ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) ) |
4 |
2 3
|
ax-mp |
⊢ ( ∅ : dom ∅ –1-1→ { 𝑥 ∈ ( 𝒫 ∅ ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ↔ ∅ : ∅ –1-1→ { 𝑥 ∈ ( 𝒫 ∅ ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) |
5 |
1 4
|
mpbir |
⊢ ∅ : dom ∅ –1-1→ { 𝑥 ∈ ( 𝒫 ∅ ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } |
6 |
|
0ex |
⊢ ∅ ∈ V |
7 |
|
vtxval0 |
⊢ ( Vtx ‘ ∅ ) = ∅ |
8 |
7
|
eqcomi |
⊢ ∅ = ( Vtx ‘ ∅ ) |
9 |
|
iedgval0 |
⊢ ( iEdg ‘ ∅ ) = ∅ |
10 |
9
|
eqcomi |
⊢ ∅ = ( iEdg ‘ ∅ ) |
11 |
8 10
|
isusgr |
⊢ ( ∅ ∈ V → ( ∅ ∈ USGraph ↔ ∅ : dom ∅ –1-1→ { 𝑥 ∈ ( 𝒫 ∅ ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) ) |
12 |
6 11
|
ax-mp |
⊢ ( ∅ ∈ USGraph ↔ ∅ : dom ∅ –1-1→ { 𝑥 ∈ ( 𝒫 ∅ ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) |
13 |
5 12
|
mpbir |
⊢ ∅ ∈ USGraph |