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

Metamath Proof Explorer

Theorem dfss7

Description: Alternate definition of subclass relationship. (Contributed by AV, 1-Aug-2022)

		Ref	Expression
	Assertion	dfss7	$⊢ B \subseteq A \leftrightarrow \{x \in A \| x \in B\} = B$

Step	Hyp	Ref	Expression
1		dfss2	$⊢ B \subseteq A \leftrightarrow B \cap A = B$
2		dfin5	$⊢ A \cap B = \{x \in A \| x \in B\}$
3	2	ineqcomi	$⊢ B \cap A = \{x \in A \| x \in B\}$
4	3	eqeq1i	$⊢ B \cap A = B \leftrightarrow \{x \in A \| x \in B\} = B$
5	1 4	bitri	$⊢ B \subseteq A \leftrightarrow \{x \in A \| x \in B\} = B$