Metamath Proof Explorer

Theorem coss2cnvepres

Description: Special case of coss1cnvres . (Contributed by Peter Mazsa, 8-Jun-2020)

Ref Expression
Assertion coss2cnvepres ⊢ ≀ E -1 ↾ A -1 = u v | u ∈ A ∧ v ∈ A ∧ ∃ x x ∈ u ∧ x ∈ v

Proof

Step Hyp Ref Expression
1 coss1cnvres ⊢ ≀ E -1 ↾ A -1 = u v | u ∈ A ∧ v ∈ A ∧ ∃ x u E -1 x ∧ v E -1 x
2 brcnvep ⊢ u ∈ V → u E -1 x ↔ x ∈ u
3 2 elv ⊢ u E -1 x ↔ x ∈ u
4 brcnvep ⊢ v ∈ V → v E -1 x ↔ x ∈ v
5 4 elv ⊢ v E -1 x ↔ x ∈ v
6 3 5 anbi12i ⊢ u E -1 x ∧ v E -1 x ↔ x ∈ u ∧ x ∈ v
7 6 exbii ⊢ ∃ x u E -1 x ∧ v E -1 x ↔ ∃ x x ∈ u ∧ x ∈ v
8 7 anbi2i ⊢ u ∈ A ∧ v ∈ A ∧ ∃ x u E -1 x ∧ v E -1 x ↔ u ∈ A ∧ v ∈ A ∧ ∃ x x ∈ u ∧ x ∈ v
9 8 opabbii ⊢ u v | u ∈ A ∧ v ∈ A ∧ ∃ x u E -1 x ∧ v E -1 x = u v | u ∈ A ∧ v ∈ A ∧ ∃ x x ∈ u ∧ x ∈ v
10 1 9 eqtri ⊢ ≀ E -1 ↾ A -1 = u v | u ∈ A ∧ v ∈ A ∧ ∃ x x ∈ u ∧ x ∈ v