This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dfrab3ss

Description: Restricted class abstraction with a common superset. (Contributed by Stefan O'Rear, 12-Sep-2015) (Proof shortened by Mario Carneiro, 8-Nov-2015)

		Ref	Expression
	Assertion	dfrab3ss	$⊢ A \subseteq B \to \{x \in A \| φ\} = A \cap \{x \in B \| φ\}$

Proof

Step	Hyp	Ref	Expression
1		dfss2	$⊢ A \subseteq B \leftrightarrow A \cap B = A$
2		ineq1	$⊢ A \cap B = A \to (A \cap B) \cap \{x \| φ\} = A \cap \{x \| φ\}$
3	2	eqcomd	$⊢ A \cap B = A \to A \cap \{x \| φ\} = (A \cap B) \cap \{x \| φ\}$
4	1 3	sylbi	$⊢ A \subseteq B \to A \cap \{x \| φ\} = (A \cap B) \cap \{x \| φ\}$
5		dfrab3	$⊢ \{x \in A \| φ\} = A \cap \{x \| φ\}$
6		dfrab3	$⊢ \{x \in B \| φ\} = B \cap \{x \| φ\}$
7	6	ineq2i	$⊢ A \cap \{x \in B \| φ\} = A \cap (B \cap \{x \| φ\})$
8		inass	$⊢ (A \cap B) \cap \{x \| φ\} = A \cap (B \cap \{x \| φ\})$
9	7 8	eqtr4i	$⊢ A \cap \{x \in B \| φ\} = (A \cap B) \cap \{x \| φ\}$
10	4 5 9	3eqtr4g	$⊢ A \subseteq B \to \{x \in A \| φ\} = A \cap \{x \in B \| φ\}$