Metamath Proof Explorer

Theorem eldmcoss2

Description: Elementhood in the domain of cosets. (Contributed by Peter Mazsa, 28-Dec-2018)

Ref Expression
Assertion eldmcoss2 ⊢ A ∈ V → A ∈ dom ⁡ ≀ R ↔ A ≀ R A

Proof

Step Hyp Ref Expression
1 eldmcoss ⊢ A ∈ V → A ∈ dom ⁡ ≀ R ↔ ∃ u u R A
2 brcoss ⊢ A ∈ V ∧ A ∈ V → A ≀ R A ↔ ∃ u u R A ∧ u R A
3 2 anidms ⊢ A ∈ V → A ≀ R A ↔ ∃ u u R A ∧ u R A
4 pm4.24 ⊢ u R A ↔ u R A ∧ u R A
5 4 exbii ⊢ ∃ u u R A ↔ ∃ u u R A ∧ u R A
6 3 5 bitr4di ⊢ A ∈ V → A ≀ R A ↔ ∃ u u R A
7 1 6 bitr4d ⊢ A ∈ V → A ∈ dom ⁡ ≀ R ↔ A ≀ R A