Description: Ordered pair membership in a composition. (Contributed by NM, 24-Feb-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | brcog | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ( 𝐶 ∘ 𝐷 ) 𝐵 ↔ ∃ 𝑥 ( 𝐴 𝐷 𝑥 ∧ 𝑥 𝐶 𝐵 ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | breq1 | ⊢ ( 𝑦 = 𝐴 → ( 𝑦 𝐷 𝑥 ↔ 𝐴 𝐷 𝑥 ) ) | |
2 | breq2 | ⊢ ( 𝑧 = 𝐵 → ( 𝑥 𝐶 𝑧 ↔ 𝑥 𝐶 𝐵 ) ) | |
3 | 1 2 | bi2anan9 | ⊢ ( ( 𝑦 = 𝐴 ∧ 𝑧 = 𝐵 ) → ( ( 𝑦 𝐷 𝑥 ∧ 𝑥 𝐶 𝑧 ) ↔ ( 𝐴 𝐷 𝑥 ∧ 𝑥 𝐶 𝐵 ) ) ) |
4 | 3 | exbidv | ⊢ ( ( 𝑦 = 𝐴 ∧ 𝑧 = 𝐵 ) → ( ∃ 𝑥 ( 𝑦 𝐷 𝑥 ∧ 𝑥 𝐶 𝑧 ) ↔ ∃ 𝑥 ( 𝐴 𝐷 𝑥 ∧ 𝑥 𝐶 𝐵 ) ) ) |
5 | df-co | ⊢ ( 𝐶 ∘ 𝐷 ) = { 〈 𝑦 , 𝑧 〉 ∣ ∃ 𝑥 ( 𝑦 𝐷 𝑥 ∧ 𝑥 𝐶 𝑧 ) } | |
6 | 4 5 | brabga | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ( 𝐶 ∘ 𝐷 ) 𝐵 ↔ ∃ 𝑥 ( 𝐴 𝐷 𝑥 ∧ 𝑥 𝐶 𝐵 ) ) ) |