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

Metamath Proof Explorer

Theorem coepr

Description: Composition with the converse membership relation. (Contributed by Scott Fenton, 18-Feb-2013)

Ref Expression
Hypotheses coep.1 ⊢ A ∈ V
coep.2 ⊢ B ∈ V
Assertion coepr ⊢ A R ∘ E -1 B ↔ ∃ x ∈ A x R B

Proof

Step Hyp Ref Expression
1 coep.1 ⊢ A ∈ V
2 coep.2 ⊢ B ∈ V
3 vex ⊢ x ∈ V
4 1 3 brcnv ⊢ A E -1 x ↔ x E A
5 1 epeli ⊢ x E A ↔ x ∈ A
6 4 5 bitri ⊢ A E -1 x ↔ x ∈ A
7 6 anbi1i ⊢ A E -1 x ∧ x R B ↔ x ∈ A ∧ x R B
8 7 exbii ⊢ ∃ x A E -1 x ∧ x R B ↔ ∃ x x ∈ A ∧ x R B
9 1 2 brco ⊢ A R ∘ E -1 B ↔ ∃ x A E -1 x ∧ x R B
10 df-rex ⊢ ∃ x ∈ A x R B ↔ ∃ x x ∈ A ∧ x R B
11 8 9 10 3bitr4i ⊢ A R ∘ E -1 B ↔ ∃ x ∈ A x R B