Metamath Proof Explorer

Theorem dfeldisj3

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

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

Proof

Step Hyp Ref Expression
1 df-eldisj ⊢ElDisjA↔DisjE-1↾A
2 relres ⊢Rel⁡E-1↾A
3 dfdisjALTV3 ⊢DisjE-1↾A↔∀u∀v∀xuE-1↾Ax∧vE-1↾Ax→u=v∧Rel⁡E-1↾A
4 2 3 mpbiran2 ⊢DisjE-1↾A↔∀u∀v∀xuE-1↾Ax∧vE-1↾Ax→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→uE-1↾Ax↔u∈A∧x∈u
7 6 el2v ⊢uE-1↾Ax↔u∈A∧x∈u
8 brcnvepres ⊢v∈V∧x∈V→vE-1↾Ax↔v∈A∧x∈v
9 8 el2v ⊢vE-1↾Ax↔v∈A∧x∈v
10 7 9 anbi12i ⊢uE-1↾Ax∧vE-1↾Ax↔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 ⊢uE-1↾Ax∧vE-1↾Ax↔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 ⊢uE-1↾Ax∧vE-1↾Ax↔u∈A∧v∈A∧x∈u∩v
16 15 imbi1i ⊢uE-1↾Ax∧vE-1↾Ax→u=v↔u∈A∧v∈A∧x∈u∩v→u=v
17 16 3albii ⊢∀u∀v∀xuE-1↾Ax∧vE-1↾Ax→u=v↔∀u∀v∀xu∈A∧v∈A∧x∈u∩v→u=v
18 1 4 17 3bitri ⊢ElDisjA↔∀u∀v∀xu∈A∧v∈A∧x∈u∩v→u=v
19 r3al ⊢∀u∈A∀v∈A∀x∈u∩vu=v↔∀u∀v∀xu∈A∧v∈A∧x∈u∩v→u=v
20 18 19 bitr4i ⊢ElDisjA↔∀u∈A∀v∈A∀x∈u∩vu=v