Metamath Proof Explorer

Theorem br1cossincnvepres

Description: B and C are cosets by an intersection with the restricted converse epsilon class: a binary relation. (Contributed by Peter Mazsa, 31-Dec-2021)

Ref Expression
Assertion br1cossincnvepres ⊢ B ∈ V ∧ C ∈ W → B ≀ R ∩ E -1 ↾ A C ↔ ∃ u ∈ A B ∈ u ∧ u R B ∧ C ∈ u ∧ u R C

Proof

Step Hyp Ref Expression
1 br1cossinres ⊢ B ∈ V ∧ C ∈ W → B ≀ R ∩ E -1 ↾ A C ↔ ∃ u ∈ A u E -1 B ∧ u R B ∧ u E -1 C ∧ u R C
2 brcnvep ⊢ u ∈ V → u E -1 B ↔ B ∈ u
3 2 elv ⊢ u E -1 B ↔ B ∈ u
4 3 anbi1i ⊢ u E -1 B ∧ u R B ↔ B ∈ u ∧ u R B
5 brcnvep ⊢ u ∈ V → u E -1 C ↔ C ∈ u
6 5 elv ⊢ u E -1 C ↔ C ∈ u
7 6 anbi1i ⊢ u E -1 C ∧ u R C ↔ C ∈ u ∧ u R C
8 4 7 anbi12i ⊢ u E -1 B ∧ u R B ∧ u E -1 C ∧ u R C ↔ B ∈ u ∧ u R B ∧ C ∈ u ∧ u R C
9 8 rexbii ⊢ ∃ u ∈ A u E -1 B ∧ u R B ∧ u E -1 C ∧ u R C ↔ ∃ u ∈ A B ∈ u ∧ u R B ∧ C ∈ u ∧ u R C
10 1 9 bitrdi ⊢ B ∈ V ∧ C ∈ W → B ≀ R ∩ E -1 ↾ A C ↔ ∃ u ∈ A B ∈ u ∧ u R B ∧ C ∈ u ∧ u R C