Metamath Proof Explorer

Theorem coep

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

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

Proof

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