Theorem intprgOLD

Description: Obsolete version of intprg as of 1-Sep-2024. (Contributed by FL, 27-Apr-2008) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	intprgOLD	$$⊢\left(A\in V\wedge B\in W\right)\to \bigcap \left\{A,B\right\}=A\cap B$$

Proof

Step	Hyp	Ref	Expression
1		preq1	$$⊢x=A\to \left\{x,y\right\}=\left\{A,y\right\}$$
2	1	inteqd	$$⊢x=A\to \bigcap \left\{x,y\right\}=\bigcap \left\{A,y\right\}$$
3		ineq1	$$⊢x=A\to x\cap y=A\cap y$$
4	2 3	eqeq12d	$$⊢x=A\to \left(\bigcap \left\{x,y\right\}=x\cap y\leftrightarrow \bigcap \left\{A,y\right\}=A\cap y\right)$$
5		preq2	$$⊢y=B\to \left\{A,y\right\}=\left\{A,B\right\}$$
6	5	inteqd	$$⊢y=B\to \bigcap \left\{A,y\right\}=\bigcap \left\{A,B\right\}$$
7		ineq2	$$⊢y=B\to A\cap y=A\cap B$$
8	6 7	eqeq12d	$$⊢y=B\to \left(\bigcap \left\{A,y\right\}=A\cap y\leftrightarrow \bigcap \left\{A,B\right\}=A\cap B\right)$$
9		vex	$$⊢x\in \mathrm{V}$$
10		vex	$$⊢y\in \mathrm{V}$$
11	9 10	intpr	$$⊢\bigcap \left\{x,y\right\}=x\cap y$$
12	4 8 11	vtocl2g	$$⊢\left(A\in V\wedge B\in W\right)\to \bigcap \left\{A,B\right\}=A\cap B$$