Metamath Proof Explorer

Theorem intprOLD

Description: Obsolete version of intpr as of 1-Sep-2024. (Contributed by NM, 14-Oct-1999) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	intpr.1	$⊢ A \in V$
		intpr.2	$⊢ B \in V$
	Assertion	intprOLD	$⊢ ⋂ \{A, B\} = A \cap B$

Proof

Step	Hyp	Ref	Expression
1		intpr.1	$⊢ A \in V$
2		intpr.2	$⊢ B \in V$
3		19.26	$⊢ \forall y ((y = A \to x \in y) \land (y = B \to x \in y)) \leftrightarrow (\forall y (y = A \to x \in y) \land \forall y (y = B \to x \in y))$
4		vex	$⊢ y \in V$
5	4	elpr	$⊢ y \in \{A, B\} \leftrightarrow (y = A \lor y = B)$
6	5	imbi1i	$⊢ (y \in \{A, B\} \to x \in y) \leftrightarrow ((y = A \lor y = B) \to x \in y)$
7		jaob	$⊢ ((y = A \lor y = B) \to x \in y) \leftrightarrow ((y = A \to x \in y) \land (y = B \to x \in y))$
8	6 7	bitri	$⊢ (y \in \{A, B\} \to x \in y) \leftrightarrow ((y = A \to x \in y) \land (y = B \to x \in y))$
9	8	albii	$⊢ \forall y (y \in \{A, B\} \to x \in y) \leftrightarrow \forall y ((y = A \to x \in y) \land (y = B \to x \in y))$
10	1	clel4	$⊢ x \in A \leftrightarrow \forall y (y = A \to x \in y)$
11	2	clel4	$⊢ x \in B \leftrightarrow \forall y (y = B \to x \in y)$
12	10 11	anbi12i	$⊢ (x \in A \land x \in B) \leftrightarrow (\forall y (y = A \to x \in y) \land \forall y (y = B \to x \in y))$
13	3 9 12	3bitr4i	$⊢ \forall y (y \in \{A, B\} \to x \in y) \leftrightarrow (x \in A \land x \in B)$
14		vex	$⊢ x \in V$
15	14	elint	$⊢ x \in ⋂ \{A, B\} \leftrightarrow \forall y (y \in \{A, B\} \to x \in y)$
16		elin	$⊢ x \in (A \cap B) \leftrightarrow (x \in A \land x \in B)$
17	13 15 16	3bitr4i	$⊢ x \in ⋂ \{A, B\} \leftrightarrow x \in (A \cap B)$
18	17	eqriv	$⊢ ⋂ \{A, B\} = A \cap B$