Theorem seeq1

Description: Equality theorem for the set-like predicate. (Contributed by Mario Carneiro, 24-Jun-2015)

	Ref	Expression
Assertion	seeq1	⊢ ( 𝑅 = 𝑆 → ( 𝑅 Se 𝐴 ↔ 𝑆 Se 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		eqimss2	⊢ ( 𝑅 = 𝑆 → 𝑆 ⊆ 𝑅 )
2		sess1	⊢ ( 𝑆 ⊆ 𝑅 → ( 𝑅 Se 𝐴 → 𝑆 Se 𝐴 ) )
3	1 2	syl	⊢ ( 𝑅 = 𝑆 → ( 𝑅 Se 𝐴 → 𝑆 Se 𝐴 ) )
4		eqimss	⊢ ( 𝑅 = 𝑆 → 𝑅 ⊆ 𝑆 )
5		sess1	⊢ ( 𝑅 ⊆ 𝑆 → ( 𝑆 Se 𝐴 → 𝑅 Se 𝐴 ) )
6	4 5	syl	⊢ ( 𝑅 = 𝑆 → ( 𝑆 Se 𝐴 → 𝑅 Se 𝐴 ) )
7	3 6	impbid	⊢ ( 𝑅 = 𝑆 → ( 𝑅 Se 𝐴 ↔ 𝑆 Se 𝐴 ) )