Step | Hyp | Ref
| Expression |
1 | | breq1 4586 |
. . 3
⊢ (𝑣 = 𝑉 → (𝑣 USGrph 𝑒 ↔ 𝑉 USGrph 𝑒)) |
2 | | difeq1 3683 |
. . . . 5
⊢ (𝑣 = 𝑉 → (𝑣 ∖ {𝑘}) = (𝑉 ∖ {𝑘})) |
3 | | reueq1 3117 |
. . . . 5
⊢ (𝑣 = 𝑉 → (∃!𝑥 ∈ 𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝑒 ↔ ∃!𝑥 ∈ 𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝑒)) |
4 | 2, 3 | raleqbidv 3129 |
. . . 4
⊢ (𝑣 = 𝑉 → (∀𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥 ∈ 𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝑒 ↔ ∀𝑙 ∈ (𝑉 ∖ {𝑘})∃!𝑥 ∈ 𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝑒)) |
5 | 4 | raleqbi1dv 3123 |
. . 3
⊢ (𝑣 = 𝑉 → (∀𝑘 ∈ 𝑣 ∀𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥 ∈ 𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝑒 ↔ ∀𝑘 ∈ 𝑉 ∀𝑙 ∈ (𝑉 ∖ {𝑘})∃!𝑥 ∈ 𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝑒)) |
6 | 1, 5 | anbi12d 743 |
. 2
⊢ (𝑣 = 𝑉 → ((𝑣 USGrph 𝑒 ∧ ∀𝑘 ∈ 𝑣 ∀𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥 ∈ 𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝑒) ↔ (𝑉 USGrph 𝑒 ∧ ∀𝑘 ∈ 𝑉 ∀𝑙 ∈ (𝑉 ∖ {𝑘})∃!𝑥 ∈ 𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝑒))) |
7 | | breq2 4587 |
. . 3
⊢ (𝑒 = 𝐸 → (𝑉 USGrph 𝑒 ↔ 𝑉 USGrph 𝐸)) |
8 | | rneq 5272 |
. . . . . 6
⊢ (𝑒 = 𝐸 → ran 𝑒 = ran 𝐸) |
9 | 8 | sseq2d 3596 |
. . . . 5
⊢ (𝑒 = 𝐸 → ({{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝑒 ↔ {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝐸)) |
10 | 9 | reubidv 3103 |
. . . 4
⊢ (𝑒 = 𝐸 → (∃!𝑥 ∈ 𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝑒 ↔ ∃!𝑥 ∈ 𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝐸)) |
11 | 10 | 2ralbidv 2972 |
. . 3
⊢ (𝑒 = 𝐸 → (∀𝑘 ∈ 𝑉 ∀𝑙 ∈ (𝑉 ∖ {𝑘})∃!𝑥 ∈ 𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝑒 ↔ ∀𝑘 ∈ 𝑉 ∀𝑙 ∈ (𝑉 ∖ {𝑘})∃!𝑥 ∈ 𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝐸)) |
12 | 7, 11 | anbi12d 743 |
. 2
⊢ (𝑒 = 𝐸 → ((𝑉 USGrph 𝑒 ∧ ∀𝑘 ∈ 𝑉 ∀𝑙 ∈ (𝑉 ∖ {𝑘})∃!𝑥 ∈ 𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝑒) ↔ (𝑉 USGrph 𝐸 ∧ ∀𝑘 ∈ 𝑉 ∀𝑙 ∈ (𝑉 ∖ {𝑘})∃!𝑥 ∈ 𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝐸))) |
13 | | df-frgra 26516 |
. 2
⊢
FriendGrph = {〈𝑣,
𝑒〉 ∣ (𝑣 USGrph 𝑒 ∧ ∀𝑘 ∈ 𝑣 ∀𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥 ∈ 𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝑒)} |
14 | 6, 12, 13 | brabg 4919 |
1
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑉 FriendGrph 𝐸 ↔ (𝑉 USGrph 𝐸 ∧ ∀𝑘 ∈ 𝑉 ∀𝑙 ∈ (𝑉 ∖ {𝑘})∃!𝑥 ∈ 𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝐸))) |