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

Metamath Proof Explorer

Theorem rcompleq

Description: Two subclasses are equal if and only if their relative complements are equal. Relativized version of compleq . (Contributed by RP, 10-Jun-2021)

		Ref	Expression
	Assertion	rcompleq	⊢ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶 ) → ( 𝐴 = 𝐵 ↔ ( 𝐶 ∖ 𝐴 ) = ( 𝐶 ∖ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ancom	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴 ) ↔ ( 𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐵 ) )
2		sscon34b	⊢ ( ( 𝐵 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐶 ) → ( 𝐵 ⊆ 𝐴 ↔ ( 𝐶 ∖ 𝐴 ) ⊆ ( 𝐶 ∖ 𝐵 ) ) )
3	2	ancoms	⊢ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶 ) → ( 𝐵 ⊆ 𝐴 ↔ ( 𝐶 ∖ 𝐴 ) ⊆ ( 𝐶 ∖ 𝐵 ) ) )
4		sscon34b	⊢ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶 ) → ( 𝐴 ⊆ 𝐵 ↔ ( 𝐶 ∖ 𝐵 ) ⊆ ( 𝐶 ∖ 𝐴 ) ) )
5	3 4	anbi12d	⊢ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶 ) → ( ( 𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐵 ) ↔ ( ( 𝐶 ∖ 𝐴 ) ⊆ ( 𝐶 ∖ 𝐵 ) ∧ ( 𝐶 ∖ 𝐵 ) ⊆ ( 𝐶 ∖ 𝐴 ) ) ) )
6	1 5	bitrid	⊢ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶 ) → ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴 ) ↔ ( ( 𝐶 ∖ 𝐴 ) ⊆ ( 𝐶 ∖ 𝐵 ) ∧ ( 𝐶 ∖ 𝐵 ) ⊆ ( 𝐶 ∖ 𝐴 ) ) ) )
7		eqss	⊢ ( 𝐴 = 𝐵 ↔ ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴 ) )
8		eqss	⊢ ( ( 𝐶 ∖ 𝐴 ) = ( 𝐶 ∖ 𝐵 ) ↔ ( ( 𝐶 ∖ 𝐴 ) ⊆ ( 𝐶 ∖ 𝐵 ) ∧ ( 𝐶 ∖ 𝐵 ) ⊆ ( 𝐶 ∖ 𝐴 ) ) )
9	6 7 8	3bitr4g	⊢ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶 ) → ( 𝐴 = 𝐵 ↔ ( 𝐶 ∖ 𝐴 ) = ( 𝐶 ∖ 𝐵 ) ) )