intmin4

Description: Elimination of a conjunct in a class intersection. (Contributed by NM, 31-Jul-2006)

		Ref	Expression
	Assertion	intmin4	$⊢ A \subseteq ⋂ \{x \| φ\} \to ⋂ \{x \| (A \subseteq x \land φ)\} = ⋂ \{x \| φ\}$

Step	Hyp	Ref	Expression
1		ssintab	$⊢ A \subseteq ⋂ \{x \| φ\} \leftrightarrow \forall x (φ \to A \subseteq x)$
2		simpr	$⊢ (A \subseteq x \land φ) \to φ$
3		ancr	$⊢ (φ \to A \subseteq x) \to (φ \to (A \subseteq x \land φ))$
4	2 3	impbid2	$⊢ (φ \to A \subseteq x) \to ((A \subseteq x \land φ) \leftrightarrow φ)$
5	4	imbi1d	$⊢ (φ \to A \subseteq x) \to (((A \subseteq x \land φ) \to y \in x) \leftrightarrow (φ \to y \in x))$
6	5	alimi	$⊢ \forall x (φ \to A \subseteq x) \to \forall x (((A \subseteq x \land φ) \to y \in x) \leftrightarrow (φ \to y \in x))$
7		albi	$⊢ \forall x (((A \subseteq x \land φ) \to y \in x) \leftrightarrow (φ \to y \in x)) \to (\forall x ((A \subseteq x \land φ) \to y \in x) \leftrightarrow \forall x (φ \to y \in x))$
8	6 7	syl	$⊢ \forall x (φ \to A \subseteq x) \to (\forall x ((A \subseteq x \land φ) \to y \in x) \leftrightarrow \forall x (φ \to y \in x))$
9	1 8	sylbi	$⊢ A \subseteq ⋂ \{x \| φ\} \to (\forall x ((A \subseteq x \land φ) \to y \in x) \leftrightarrow \forall x (φ \to y \in x))$
10		vex	$⊢ y \in V$
11	10	elintab	$⊢ y \in ⋂ \{x \| (A \subseteq x \land φ)\} \leftrightarrow \forall x ((A \subseteq x \land φ) \to y \in x)$
12	10	elintab	$⊢ y \in ⋂ \{x \| φ\} \leftrightarrow \forall x (φ \to y \in x)$
13	9 11 12	3bitr4g	$⊢ A \subseteq ⋂ \{x \| φ\} \to (y \in ⋂ \{x \| (A \subseteq x \land φ)\} \leftrightarrow y \in ⋂ \{x \| φ\})$
14	13	eqrdv	$⊢ A \subseteq ⋂ \{x \| φ\} \to ⋂ \{x \| (A \subseteq x \land φ)\} = ⋂ \{x \| φ\}$

Metamath Proof Explorer