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 ∈ V ∧ B ∈ W → A R ∩ B R = ∅ ↔ ∀ x A R x → ¬ B R x

Proof

Step Hyp Ref Expression
1 disj1 ⊢ A R ∩ B R = ∅ ↔ ∀ x x ∈ A R → ¬ x ∈ B R
2 elecg ⊢ x ∈ V ∧ A ∈ V → x ∈ A R ↔ A R x
3 2 el2v1 ⊢ A ∈ V → x ∈ A R ↔ A R x
4 3 adantr ⊢ A ∈ V ∧ B ∈ W → x ∈ A R ↔ A R x
5 elecALTV ⊢ B ∈ W ∧ x ∈ V → x ∈ B R ↔ B R x
6 5 elvd ⊢ B ∈ W → x ∈ B R ↔ B R x
7 6 adantl ⊢ A ∈ V ∧ B ∈ W → x ∈ B R ↔ B R x
8 7 notbid ⊢ A ∈ V ∧ B ∈ W → ¬ x ∈ B R ↔ ¬ B R x
9 4 8 imbi12d ⊢ A ∈ V ∧ B ∈ W → x ∈ A R → ¬ x ∈ B R ↔ A R x → ¬ B R x
10 9 albidv ⊢ A ∈ V ∧ B ∈ W → ∀ x x ∈ A R → ¬ x ∈ B R ↔ ∀ x A R x → ¬ B R x
11 1 10 syl5bb ⊢ A ∈ V ∧ B ∈ W → A R ∩ B R = ∅ ↔ ∀ x A R x → ¬ B R x