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	⊢ ( 𝐴 = 𝐵 → ≀ 𝐴 = ≀ 𝐵 )