Theorem coepr

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

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

Proof

Step	Hyp	Ref	Expression
1		coep.1	⊢ 𝐴 ∈ V
2		coep.2	⊢ 𝐵 ∈ V
3		vex	⊢ 𝑥 ∈ V
4	1 3	brcnv	⊢ ( 𝐴 ◡ E 𝑥 ↔ 𝑥 E 𝐴 )
5	1	epeli	⊢ ( 𝑥 E 𝐴 ↔ 𝑥 ∈ 𝐴 )
6	4 5	bitri	⊢ ( 𝐴 ◡ E 𝑥 ↔ 𝑥 ∈ 𝐴 )
7	6	anbi1i	⊢ ( ( 𝐴 ◡ E 𝑥 ∧ 𝑥 𝑅 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝐵 ) )
8	7	exbii	⊢ ( ∃ 𝑥 ( 𝐴 ◡ E 𝑥 ∧ 𝑥 𝑅 𝐵 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝐵 ) )
9	1 2	brco	⊢ ( 𝐴 ( 𝑅 ∘ ◡ E ) 𝐵 ↔ ∃ 𝑥 ( 𝐴 ◡ E 𝑥 ∧ 𝑥 𝑅 𝐵 ) )
10		df-rex	⊢ ( ∃ 𝑥 ∈ 𝐴 𝑥 𝑅 𝐵 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝐵 ) )
11	8 9 10	3bitr4i	⊢ ( 𝐴 ( 𝑅 ∘ ◡ E ) 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 𝑥 𝑅 𝐵 )