Metamath Proof Explorer


Theorem sess2

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

Ref Expression
Assertion sess2 ABRSeBRSeA

Proof

Step Hyp Ref Expression
1 ssralv ABxByB|yRxVxAyB|yRxV
2 rabss2 AByA|yRxyB|yRx
3 ssexg yA|yRxyB|yRxyB|yRxVyA|yRxV
4 3 ex yA|yRxyB|yRxyB|yRxVyA|yRxV
5 2 4 syl AByB|yRxVyA|yRxV
6 5 ralimdv ABxAyB|yRxVxAyA|yRxV
7 1 6 syld ABxByB|yRxVxAyA|yRxV
8 df-se RSeBxByB|yRxV
9 df-se RSeAxAyA|yRxV
10 7 8 9 3imtr4g ABRSeBRSeA