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	|- ( ( A e. V /\ B e. W ) -> |^| { A , B } = ( A i^i B ) )

Proof

Step	Hyp	Ref	Expression
1		preq1	|- ( x = A -> { x , y } = { A , y } )
2	1	inteqd	|- ( x = A -> |^| { x , y } = |^| { A , y } )
3		ineq1	|- ( x = A -> ( x i^i y ) = ( A i^i y ) )
4	2 3	eqeq12d	|- ( x = A -> ( |^| { x , y } = ( x i^i y ) <-> |^| { A , y } = ( A i^i y ) ) )
5		preq2	|- ( y = B -> { A , y } = { A , B } )
6	5	inteqd	|- ( y = B -> |^| { A , y } = |^| { A , B } )
7		ineq2	|- ( y = B -> ( A i^i y ) = ( A i^i B ) )
8	6 7	eqeq12d	|- ( y = B -> ( |^| { A , y } = ( A i^i y ) <-> |^| { A , B } = ( A i^i B ) ) )
9		vex	|- x e. _V
10		vex	|- y e. _V
11	9 10	intpr	|- |^| { x , y } = ( x i^i y )
12	4 8 11	vtocl2g	|- ( ( A e. V /\ B e. W ) -> |^| { A , B } = ( A i^i B ) )