Theorem extssr

Description: Property of subset relation, see also extid , extep and the comment of df-ssr . (Contributed by Peter Mazsa, 10-Jul-2019)

	Ref	Expression
Assertion	extssr	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( [ 𝐴 ] ◡ S = [ 𝐵 ] ◡ S ↔ 𝐴 = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		brssr	⊢ ( 𝐴 ∈ 𝑉 → ( 𝑥 S 𝐴 ↔ 𝑥 ⊆ 𝐴 ) )
2		brssr	⊢ ( 𝐵 ∈ 𝑊 → ( 𝑥 S 𝐵 ↔ 𝑥 ⊆ 𝐵 ) )
3	1 2	bi2bian9	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( 𝑥 S 𝐴 ↔ 𝑥 S 𝐵 ) ↔ ( 𝑥 ⊆ 𝐴 ↔ 𝑥 ⊆ 𝐵 ) ) )
4	3	albidv	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ∀ 𝑥 ( 𝑥 S 𝐴 ↔ 𝑥 S 𝐵 ) ↔ ∀ 𝑥 ( 𝑥 ⊆ 𝐴 ↔ 𝑥 ⊆ 𝐵 ) ) )
5		relssr	⊢ Rel S
6		releccnveq	⊢ ( ( Rel S ∧ Rel S ) → ( [ 𝐴 ] ◡ S = [ 𝐵 ] ◡ S ↔ ∀ 𝑥 ( 𝑥 S 𝐴 ↔ 𝑥 S 𝐵 ) ) )
7	5 5 6	mp2an	⊢ ( [ 𝐴 ] ◡ S = [ 𝐵 ] ◡ S ↔ ∀ 𝑥 ( 𝑥 S 𝐴 ↔ 𝑥 S 𝐵 ) )
8		ssext	⊢ ( 𝐴 = 𝐵 ↔ ∀ 𝑥 ( 𝑥 ⊆ 𝐴 ↔ 𝑥 ⊆ 𝐵 ) )
9	4 7 8	3bitr4g	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( [ 𝐴 ] ◡ S = [ 𝐵 ] ◡ S ↔ 𝐴 = 𝐵 ) )