Theorem coep

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

	Ref	Expression
Hypotheses	coep.1	⊢ 𝐴 ∈ V
	coep.2	⊢ 𝐵 ∈ V
Assertion	coep	⊢ ( 𝐴 ( E ∘ 𝑅 ) 𝐵 ↔ ∃ 𝑥 ∈ 𝐵 𝐴 𝑅 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		coep.1	⊢ 𝐴 ∈ V
2		coep.2	⊢ 𝐵 ∈ V
3	2	epeli	⊢ ( 𝑥 E 𝐵 ↔ 𝑥 ∈ 𝐵 )
4	3	anbi1ci	⊢ ( ( 𝐴 𝑅 𝑥 ∧ 𝑥 E 𝐵 ) ↔ ( 𝑥 ∈ 𝐵 ∧ 𝐴 𝑅 𝑥 ) )
5	4	exbii	⊢ ( ∃ 𝑥 ( 𝐴 𝑅 𝑥 ∧ 𝑥 E 𝐵 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝐴 𝑅 𝑥 ) )
6	1 2	brco	⊢ ( 𝐴 ( E ∘ 𝑅 ) 𝐵 ↔ ∃ 𝑥 ( 𝐴 𝑅 𝑥 ∧ 𝑥 E 𝐵 ) )
7		df-rex	⊢ ( ∃ 𝑥 ∈ 𝐵 𝐴 𝑅 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝐴 𝑅 𝑥 ) )
8	5 6 7	3bitr4i	⊢ ( 𝐴 ( E ∘ 𝑅 ) 𝐵 ↔ ∃ 𝑥 ∈ 𝐵 𝐴 𝑅 𝑥 )