This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cosseq

Description: Equality theorem for the classes of cosets by A and B . (Contributed by Peter Mazsa, 9-Jan-2018)

Ref Expression
Assertion cosseq ( 𝐴 = 𝐵 → ≀ 𝐴 = ≀ 𝐵 )

Proof

Step Hyp Ref Expression
1 breq ⊢ ( 𝐴 = 𝐵 → ( 𝑢 𝐴 𝑥 ↔ 𝑢 𝐵 𝑥 ) )
2 breq ⊢ ( 𝐴 = 𝐵 → ( 𝑢 𝐴 𝑦 ↔ 𝑢 𝐵 𝑦 ) )
3 1 2 anbi12d ⊢ ( 𝐴 = 𝐵 → ( ( 𝑢 𝐴 𝑥 ∧ 𝑢 𝐴 𝑦 ) ↔ ( 𝑢 𝐵 𝑥 ∧ 𝑢 𝐵 𝑦 ) ) )
4 3 exbidv ⊢ ( 𝐴 = 𝐵 → ( ∃ 𝑢 ( 𝑢 𝐴 𝑥 ∧ 𝑢 𝐴 𝑦 ) ↔ ∃ 𝑢 ( 𝑢 𝐵 𝑥 ∧ 𝑢 𝐵 𝑦 ) ) )
5 4 opabbidv ⊢ ( 𝐴 = 𝐵 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ( 𝑢 𝐴 𝑥 ∧ 𝑢 𝐴 𝑦 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ( 𝑢 𝐵 𝑥 ∧ 𝑢 𝐵 𝑦 ) } )
6 df-coss ⊢ ≀ 𝐴 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ( 𝑢 𝐴 𝑥 ∧ 𝑢 𝐴 𝑦 ) }
7 df-coss ⊢ ≀ 𝐵 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ( 𝑢 𝐵 𝑥 ∧ 𝑢 𝐵 𝑦 ) }
8 5 6 7 3eqtr4g ⊢ ( 𝐴 = 𝐵 → ≀ 𝐴 = ≀ 𝐵 )