Metamath Proof Explorer


Theorem dfeldisj5

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

Ref Expression
Assertion dfeldisj5 ElDisj A u A v A u = v u v =

Proof

Step Hyp Ref Expression
1 dfeldisj4 ElDisj A x * u A x u
2 inecmo2 u A v A u = v u E -1 v E -1 = Rel E -1 x * u A u E -1 x Rel E -1
3 relcnv Rel E -1
4 3 biantru u A v A u = v u E -1 v E -1 = u A v A u = v u E -1 v E -1 = Rel E -1
5 3 biantru x * u A u E -1 x x * u A u E -1 x Rel E -1
6 2 4 5 3bitr4i u A v A u = v u E -1 v E -1 = x * u A u E -1 x
7 eccnvep u V u E -1 = u
8 7 elv u E -1 = u
9 eccnvep v V v E -1 = v
10 9 elv v E -1 = v
11 8 10 ineq12i u E -1 v E -1 = u v
12 11 eqeq1i u E -1 v E -1 = u v =
13 12 orbi2i u = v u E -1 v E -1 = u = v u v =
14 13 2ralbii u A v A u = v u E -1 v E -1 = u A v A u = v u v =
15 brcnvep u V u E -1 x x u
16 15 elv u E -1 x x u
17 16 rmobii * u A u E -1 x * u A x u
18 17 albii x * u A u E -1 x x * u A x u
19 6 14 18 3bitr3i u A v A u = v u v = x * u A x u
20 1 19 bitr4i ElDisj A u A v A u = v u v =