Theorem opelco

Description: Ordered pair membership in a composition. (Contributed by NM, 27-Dec-1996) (Revised by Mario Carneiro, 24-Feb-2015)

	Ref	Expression
Hypotheses	opelco.1	⊢ 𝐴 ∈ V
	opelco.2	⊢ 𝐵 ∈ V
Assertion	opelco	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝐶 ∘ 𝐷 ) ↔ ∃ 𝑥 ( 𝐴 𝐷 𝑥 ∧ 𝑥 𝐶 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		opelco.1	⊢ 𝐴 ∈ V
2		opelco.2	⊢ 𝐵 ∈ V
3		df-br	⊢ ( 𝐴 ( 𝐶 ∘ 𝐷 ) 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝐶 ∘ 𝐷 ) )
4	1 2	brco	⊢ ( 𝐴 ( 𝐶 ∘ 𝐷 ) 𝐵 ↔ ∃ 𝑥 ( 𝐴 𝐷 𝑥 ∧ 𝑥 𝐶 𝐵 ) )
5	3 4	bitr3i	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝐶 ∘ 𝐷 ) ↔ ∃ 𝑥 ( 𝐴 𝐷 𝑥 ∧ 𝑥 𝐶 𝐵 ) )