subsubrg2

Description: The set of subrings of a subring are the smaller subrings. (Contributed by Stefan O'Rear, 9-Mar-2015)

		Ref	Expression
	Hypothesis	subsubrg.s	$⊢ S = R ↾_{𝑠} A$
	Assertion	subsubrg2	$⊢ A \in SubRing (R) \to SubRing (S) = SubRing (R) \cap 𝒫 A$

Step	Hyp	Ref	Expression
1		subsubrg.s	$⊢ S = R ↾_{𝑠} A$
2	1	subsubrg	$⊢ A \in SubRing (R) \to (a \in SubRing (S) \leftrightarrow (a \in SubRing (R) \land a \subseteq A))$
3		elin	$⊢ a \in (SubRing (R) \cap 𝒫 A) \leftrightarrow (a \in SubRing (R) \land a \in 𝒫 A)$
4		velpw	$⊢ a \in 𝒫 A \leftrightarrow a \subseteq A$
5	4	anbi2i	$⊢ (a \in SubRing (R) \land a \in 𝒫 A) \leftrightarrow (a \in SubRing (R) \land a \subseteq A)$
6	3 5	bitr2i	$⊢ (a \in SubRing (R) \land a \subseteq A) \leftrightarrow a \in (SubRing (R) \cap 𝒫 A)$
7	2 6	bitrdi	$⊢ A \in SubRing (R) \to (a \in SubRing (S) \leftrightarrow a \in (SubRing (R) \cap 𝒫 A))$
8	7	eqrdv	$⊢ A \in SubRing (R) \to SubRing (S) = SubRing (R) \cap 𝒫 A$

Metamath Proof Explorer