sess2

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

		Ref	Expression
	Assertion	sess2	$⊢ A \subseteq B \to (R Se B \to R Se A)$

Step	Hyp	Ref	Expression
1		ssralv	$⊢ A \subseteq B \to (\forall x \in B \{y \in B \| y R x\} \in V \to \forall x \in A \{y \in B \| y R x\} \in V)$
2		rabss2	$⊢ A \subseteq B \to \{y \in A \| y R x\} \subseteq \{y \in B \| y R x\}$
3		ssexg	$⊢ (\{y \in A \| y R x\} \subseteq \{y \in B \| y R x\} \land \{y \in B \| y R x\} \in V) \to \{y \in A \| y R x\} \in V$
4	3	ex	$⊢ \{y \in A \| y R x\} \subseteq \{y \in B \| y R x\} \to (\{y \in B \| y R x\} \in V \to \{y \in A \| y R x\} \in V)$
5	2 4	syl	$⊢ A \subseteq B \to (\{y \in B \| y R x\} \in V \to \{y \in A \| y R x\} \in V)$
6	5	ralimdv	$⊢ A \subseteq B \to (\forall x \in A \{y \in B \| y R x\} \in V \to \forall x \in A \{y \in A \| y R x\} \in V)$
7	1 6	syld	$⊢ A \subseteq B \to (\forall x \in B \{y \in B \| y R x\} \in V \to \forall x \in A \{y \in A \| y R x\} \in V)$
8		df-se	$⊢ R Se B \leftrightarrow \forall x \in B \{y \in B \| y R x\} \in V$
9		df-se	$⊢ R Se A \leftrightarrow \forall x \in A \{y \in A \| y R x\} \in V$
10	7 8 9	3imtr4g	$⊢ A \subseteq B \to (R Se B \to R Se A)$

Metamath Proof Explorer