bj-restb

Description: An elementwise intersection by a set on a family containing a superset of that set contains that set. (Contributed by BJ, 27-Apr-2021)

		Ref	Expression
	Assertion	bj-restb	$⊢ X \in V \to ((A \subseteq B \land B \in X) \to A \in (X ↾_{𝑡} A))$

Proof

Step	Hyp	Ref	Expression
1		id	$⊢ A \subseteq B \to A \subseteq B$
2		ssidd	$⊢ A \subseteq B \to A \subseteq A$
3	1 2	ssind	$⊢ A \subseteq B \to A \subseteq B \cap A$
4		inss2	$⊢ B \cap A \subseteq A$
5	4	a1i	$⊢ A \subseteq B \to B \cap A \subseteq A$
6	3 5	eqssd	$⊢ A \subseteq B \to A = B \cap A$
7		eleq1	$⊢ y = B \to (y \in X \leftrightarrow B \in X)$
8		ineq1	$⊢ y = B \to y \cap A = B \cap A$
9	8	eqeq2d	$⊢ y = B \to (A = y \cap A \leftrightarrow A = B \cap A)$
10	7 9	anbi12d	$⊢ y = B \to ((y \in X \land A = y \cap A) \leftrightarrow (B \in X \land A = B \cap A))$
11	10	spcegv	$⊢ B \in X \to ((B \in X \land A = B \cap A) \to \exists y (y \in X \land A = y \cap A))$
12	11	expd	$⊢ B \in X \to (B \in X \to (A = B \cap A \to \exists y (y \in X \land A = y \cap A)))$
13	12	pm2.43i	$⊢ B \in X \to (A = B \cap A \to \exists y (y \in X \land A = y \cap A))$
14	6 13	mpan9	$⊢ (A \subseteq B \land B \in X) \to \exists y (y \in X \land A = y \cap A)$
15		df-rex	$⊢ \exists y \in X A = y \cap A \leftrightarrow \exists y (y \in X \land A = y \cap A)$
16	14 15	sylibr	$⊢ (A \subseteq B \land B \in X) \to \exists y \in X A = y \cap A$
17	16	adantl	$⊢ (X \in V \land (A \subseteq B \land B \in X)) \to \exists y \in X A = y \cap A$
18		ssexg	$⊢ (A \subseteq B \land B \in X) \to A \in V$
19		elrest	$⊢ (X \in V \land A \in V) \to (A \in (X ↾_{𝑡} A) \leftrightarrow \exists y \in X A = y \cap A)$
20	18 19	sylan2	$⊢ (X \in V \land (A \subseteq B \land B \in X)) \to (A \in (X ↾_{𝑡} A) \leftrightarrow \exists y \in X A = y \cap A)$
21	17 20	mpbird	$⊢ (X \in V \land (A \subseteq B \land B \in X)) \to A \in (X ↾_{𝑡} A)$
22	21	ex	$⊢ X \in V \to ((A \subseteq B \land B \in X) \to A \in (X ↾_{𝑡} A))$

Metamath Proof Explorer

Theorem bj-restb

Proof