Metamath Proof Explorer

Theorem dfeldisj3

Description: Alternate definition of the disjoint elementhood predicate. (Contributed by Peter Mazsa, 19-Sep-2021)

Ref Expression
Assertion dfeldisj3 ⊢ ElDisj A ↔ ∀ u ∈ A ∀ v ∈ A ∀ x ∈ u ∩ v u = v

Proof

Step Hyp Ref Expression
1 df-eldisj ⊢ ElDisj A ↔ Disj E -1 ↾ A
2 relres ⊢ Rel ⁡ E -1 ↾ A
3 dfdisjALTV3 ⊢ Disj E -1 ↾ A ↔ ∀ u ∀ v ∀ x u E -1 ↾ A x ∧ v E -1 ↾ A x → u = v ∧ Rel ⁡ E -1 ↾ A
4 2 3 mpbiran2 ⊢ Disj E -1 ↾ A ↔ ∀ u ∀ v ∀ x u E -1 ↾ A x ∧ v E -1 ↾ A x → u = v
5 an4 ⊢ u ∈ A ∧ x ∈ u ∧ v ∈ A ∧ x ∈ v ↔ u ∈ A ∧ v ∈ A ∧ x ∈ u ∧ x ∈ v
6 brcnvepres ⊢ u ∈ V ∧ x ∈ V → u E -1 ↾ A x ↔ u ∈ A ∧ x ∈ u
7 6 el2v ⊢ u E -1 ↾ A x ↔ u ∈ A ∧ x ∈ u
8 brcnvepres ⊢ v ∈ V ∧ x ∈ V → v E -1 ↾ A x ↔ v ∈ A ∧ x ∈ v
9 8 el2v ⊢ v E -1 ↾ A x ↔ v ∈ A ∧ x ∈ v
10 7 9 anbi12i ⊢ u E -1 ↾ A x ∧ v E -1 ↾ A x ↔ u ∈ A ∧ x ∈ u ∧ v ∈ A ∧ x ∈ v
11 elin ⊢ x ∈ u ∩ v ↔ x ∈ u ∧ x ∈ v
12 11 anbi2i ⊢ u ∈ A ∧ v ∈ A ∧ x ∈ u ∩ v ↔ u ∈ A ∧ v ∈ A ∧ x ∈ u ∧ x ∈ v
13 5 10 12 3bitr4i ⊢ u E -1 ↾ A x ∧ v E -1 ↾ A x ↔ u ∈ A ∧ v ∈ A ∧ x ∈ u ∩ v
14 df-3an ⊢ u ∈ A ∧ v ∈ A ∧ x ∈ u ∩ v ↔ u ∈ A ∧ v ∈ A ∧ x ∈ u ∩ v
15 13 14 bitr4i ⊢ u E -1 ↾ A x ∧ v E -1 ↾ A x ↔ u ∈ A ∧ v ∈ A ∧ x ∈ u ∩ v
16 15 imbi1i ⊢ u E -1 ↾ A x ∧ v E -1 ↾ A x → u = v ↔ u ∈ A ∧ v ∈ A ∧ x ∈ u ∩ v → u = v
17 16 3albii ⊢ ∀ u ∀ v ∀ x u E -1 ↾ A x ∧ v E -1 ↾ A x → u = v ↔ ∀ u ∀ v ∀ x u ∈ A ∧ v ∈ A ∧ x ∈ u ∩ v → u = v
18 1 4 17 3bitri ⊢ ElDisj A ↔ ∀ u ∀ v ∀ x u ∈ A ∧ v ∈ A ∧ x ∈ u ∩ v → u = v
19 r3al ⊢ ∀ u ∈ A ∀ v ∈ A ∀ x ∈ u ∩ v u = v ↔ ∀ u ∀ v ∀ x u ∈ A ∧ v ∈ A ∧ x ∈ u ∩ v → u = v
20 18 19 bitr4i ⊢ ElDisj A ↔ ∀ u ∈ A ∀ v ∈ A ∀ x ∈ u ∩ v u = v