# Metamath Proof Explorer

## Theorem mdi

Description: Consequence of the modular pair property. (Contributed by NM, 22-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion mdi ( ( ( 𝐴C𝐵C𝐶C ) ∧ ( 𝐴 𝑀 𝐵𝐶𝐵 ) ) → ( ( 𝐶 𝐴 ) ∩ 𝐵 ) = ( 𝐶 ( 𝐴𝐵 ) ) )

### Proof

Step Hyp Ref Expression
1 mdbr ( ( 𝐴C𝐵C ) → ( 𝐴 𝑀 𝐵 ↔ ∀ 𝑥C ( 𝑥𝐵 → ( ( 𝑥 𝐴 ) ∩ 𝐵 ) = ( 𝑥 ( 𝐴𝐵 ) ) ) ) )
2 1 biimpd ( ( 𝐴C𝐵C ) → ( 𝐴 𝑀 𝐵 → ∀ 𝑥C ( 𝑥𝐵 → ( ( 𝑥 𝐴 ) ∩ 𝐵 ) = ( 𝑥 ( 𝐴𝐵 ) ) ) ) )
3 sseq1 ( 𝑥 = 𝐶 → ( 𝑥𝐵𝐶𝐵 ) )
4 oveq1 ( 𝑥 = 𝐶 → ( 𝑥 𝐴 ) = ( 𝐶 𝐴 ) )
5 4 ineq1d ( 𝑥 = 𝐶 → ( ( 𝑥 𝐴 ) ∩ 𝐵 ) = ( ( 𝐶 𝐴 ) ∩ 𝐵 ) )
6 oveq1 ( 𝑥 = 𝐶 → ( 𝑥 ( 𝐴𝐵 ) ) = ( 𝐶 ( 𝐴𝐵 ) ) )
7 5 6 eqeq12d ( 𝑥 = 𝐶 → ( ( ( 𝑥 𝐴 ) ∩ 𝐵 ) = ( 𝑥 ( 𝐴𝐵 ) ) ↔ ( ( 𝐶 𝐴 ) ∩ 𝐵 ) = ( 𝐶 ( 𝐴𝐵 ) ) ) )
8 3 7 imbi12d ( 𝑥 = 𝐶 → ( ( 𝑥𝐵 → ( ( 𝑥 𝐴 ) ∩ 𝐵 ) = ( 𝑥 ( 𝐴𝐵 ) ) ) ↔ ( 𝐶𝐵 → ( ( 𝐶 𝐴 ) ∩ 𝐵 ) = ( 𝐶 ( 𝐴𝐵 ) ) ) ) )
9 8 rspcv ( 𝐶C → ( ∀ 𝑥C ( 𝑥𝐵 → ( ( 𝑥 𝐴 ) ∩ 𝐵 ) = ( 𝑥 ( 𝐴𝐵 ) ) ) → ( 𝐶𝐵 → ( ( 𝐶 𝐴 ) ∩ 𝐵 ) = ( 𝐶 ( 𝐴𝐵 ) ) ) ) )
10 2 9 sylan9 ( ( ( 𝐴C𝐵C ) ∧ 𝐶C ) → ( 𝐴 𝑀 𝐵 → ( 𝐶𝐵 → ( ( 𝐶 𝐴 ) ∩ 𝐵 ) = ( 𝐶 ( 𝐴𝐵 ) ) ) ) )
11 10 3impa ( ( 𝐴C𝐵C𝐶C ) → ( 𝐴 𝑀 𝐵 → ( 𝐶𝐵 → ( ( 𝐶 𝐴 ) ∩ 𝐵 ) = ( 𝐶 ( 𝐴𝐵 ) ) ) ) )
12 11 imp32 ( ( ( 𝐴C𝐵C𝐶C ) ∧ ( 𝐴 𝑀 𝐵𝐶𝐵 ) ) → ( ( 𝐶 𝐴 ) ∩ 𝐵 ) = ( 𝐶 ( 𝐴𝐵 ) ) )