This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ecin0

Description: Two ways of saying that the coset of A and the coset of B have no elements in common. (Contributed by Peter Mazsa, 1-Dec-2018)

Ref Expression
Assertion ecin0 
|- ( ( A e. V /\ B e. W ) -> ( ( [ A ] R i^i [ B ] R ) = (/) <-> A. x ( A R x -> -. B R x ) ) )

Proof

Step Hyp Ref Expression
1 disj1 
 |-  ( ( [ A ] R i^i [ B ] R ) = (/) <-> A. x ( x e. [ A ] R -> -. x e. [ B ] R ) )
2 elecg 
 |-  ( ( x e. _V /\ A e. V ) -> ( x e. [ A ] R <-> A R x ) )
3 2 el2v1 
 |-  ( A e. V -> ( x e. [ A ] R <-> A R x ) )
4 3 adantr 
 |-  ( ( A e. V /\ B e. W ) -> ( x e. [ A ] R <-> A R x ) )
5 elecALTV 
 |-  ( ( B e. W /\ x e. _V ) -> ( x e. [ B ] R <-> B R x ) )
6 5 elvd 
 |-  ( B e. W -> ( x e. [ B ] R <-> B R x ) )
7 6 adantl 
 |-  ( ( A e. V /\ B e. W ) -> ( x e. [ B ] R <-> B R x ) )
8 7 notbid 
 |-  ( ( A e. V /\ B e. W ) -> ( -. x e. [ B ] R <-> -. B R x ) )
9 4 8 imbi12d 
 |-  ( ( A e. V /\ B e. W ) -> ( ( x e. [ A ] R -> -. x e. [ B ] R ) <-> ( A R x -> -. B R x ) ) )
10 9 albidv 
 |-  ( ( A e. V /\ B e. W ) -> ( A. x ( x e. [ A ] R -> -. x e. [ B ] R ) <-> A. x ( A R x -> -. B R x ) ) )
11 1 10 bitrid 
 |-  ( ( A e. V /\ B e. W ) -> ( ( [ A ] R i^i [ B ] R ) = (/) <-> A. x ( A R x -> -. B R x ) ) )