Theorem opelco2g

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

	Ref	Expression
Assertion	opelco2g	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝐶 ∘ 𝐷 ) ↔ ∃ 𝑥 ( ⟨ 𝐴 , 𝑥 ⟩ ∈ 𝐷 ∧ ⟨ 𝑥 , 𝐵 ⟩ ∈ 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		brcog	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ( 𝐶 ∘ 𝐷 ) 𝐵 ↔ ∃ 𝑥 ( 𝐴 𝐷 𝑥 ∧ 𝑥 𝐶 𝐵 ) ) )
2		df-br	⊢ ( 𝐴 ( 𝐶 ∘ 𝐷 ) 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝐶 ∘ 𝐷 ) )
3		df-br	⊢ ( 𝐴 𝐷 𝑥 ↔ ⟨ 𝐴 , 𝑥 ⟩ ∈ 𝐷 )
4		df-br	⊢ ( 𝑥 𝐶 𝐵 ↔ ⟨ 𝑥 , 𝐵 ⟩ ∈ 𝐶 )
5	3 4	anbi12i	⊢ ( ( 𝐴 𝐷 𝑥 ∧ 𝑥 𝐶 𝐵 ) ↔ ( ⟨ 𝐴 , 𝑥 ⟩ ∈ 𝐷 ∧ ⟨ 𝑥 , 𝐵 ⟩ ∈ 𝐶 ) )
6	5	exbii	⊢ ( ∃ 𝑥 ( 𝐴 𝐷 𝑥 ∧ 𝑥 𝐶 𝐵 ) ↔ ∃ 𝑥 ( ⟨ 𝐴 , 𝑥 ⟩ ∈ 𝐷 ∧ ⟨ 𝑥 , 𝐵 ⟩ ∈ 𝐶 ) )
7	1 2 6	3bitr3g	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝐶 ∘ 𝐷 ) ↔ ∃ 𝑥 ( ⟨ 𝐴 , 𝑥 ⟩ ∈ 𝐷 ∧ ⟨ 𝑥 , 𝐵 ⟩ ∈ 𝐶 ) ) )