sess1

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

		Ref	Expression
	Assertion	sess1	$⊢ R \subseteq S \to (S Se A \to R Se A)$

Step	Hyp	Ref	Expression
1		simpl	$⊢ (R \subseteq S \land y \in A) \to R \subseteq S$
2	1	ssbrd	$⊢ (R \subseteq S \land y \in A) \to (y R x \to y S x)$
3	2	ss2rabdv	$⊢ R \subseteq S \to \{y \in A \| y R x\} \subseteq \{y \in A \| y S x\}$
4		ssexg	$⊢ (\{y \in A \| y R x\} \subseteq \{y \in A \| y S x\} \land \{y \in A \| y S x\} \in V) \to \{y \in A \| y R x\} \in V$
5	4	ex	$⊢ \{y \in A \| y R x\} \subseteq \{y \in A \| y S x\} \to (\{y \in A \| y S x\} \in V \to \{y \in A \| y R x\} \in V)$
6	3 5	syl	$⊢ R \subseteq S \to (\{y \in A \| y S x\} \in V \to \{y \in A \| y R x\} \in V)$
7	6	ralimdv	$⊢ R \subseteq S \to (\forall x \in A \{y \in A \| y S x\} \in V \to \forall x \in A \{y \in A \| y R x\} \in V)$
8		df-se	$⊢ S Se A \leftrightarrow \forall x \in A \{y \in A \| y S 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	$⊢ R \subseteq S \to (S Se A \to R Se A)$

Metamath Proof Explorer