Theorem bj-projeq

Description: Substitution property for Proj . (Contributed by BJ, 6-Apr-2019)

	Ref	Expression
Assertion	bj-projeq	|- ( A = C -> ( B = D -> ( A Proj B ) = ( C Proj D ) ) )

Proof

Step	Hyp	Ref	Expression
1		simpr	|- ( ( A = C /\ B = D ) -> B = D )
2		simpl	|- ( ( A = C /\ B = D ) -> A = C )
3	2	sneqd	|- ( ( A = C /\ B = D ) -> { A } = { C } )
4	1 3	imaeq12d	|- ( ( A = C /\ B = D ) -> ( B " { A } ) = ( D " { C } ) )
5	4	eleq2d	|- ( ( A = C /\ B = D ) -> ( { x } e. ( B " { A } ) <-> { x } e. ( D " { C } ) ) )
6	5	abbidv	|- ( ( A = C /\ B = D ) -> { x | { x } e. ( B " { A } ) } = { x | { x } e. ( D " { C } ) } )
7		df-bj-proj	|- ( A Proj B ) = { x | { x } e. ( B " { A } ) }
8		df-bj-proj	|- ( C Proj D ) = { x | { x } e. ( D " { C } ) }
9	6 7 8	3eqtr4g	|- ( ( A = C /\ B = D ) -> ( A Proj B ) = ( C Proj D ) )
10	9	ex	|- ( A = C -> ( B = D -> ( A Proj B ) = ( C Proj D ) ) )