Theorem mptssid

Description: The mapping operation expressed with its actual domain. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	mptssid.1	|- F/_ x A
	mptssid.2	|- C = { x e. A | B e. _V }
Assertion	mptssid	|- ( x e. A |-> B ) = ( x e. C |-> B )

Proof

Step	Hyp	Ref	Expression
1		mptssid.1	|- F/_ x A
2		mptssid.2	|- C = { x e. A | B e. _V }
3		eqvisset	|- ( y = B -> B e. _V )
4	3	anim2i	|- ( ( x e. A /\ y = B ) -> ( x e. A /\ B e. _V ) )
5		rabid	|- ( x e. { x e. A | B e. _V } <-> ( x e. A /\ B e. _V ) )
6	4 5	sylibr	|- ( ( x e. A /\ y = B ) -> x e. { x e. A | B e. _V } )
7	6 2	eleqtrrdi	|- ( ( x e. A /\ y = B ) -> x e. C )
8		simpr	|- ( ( x e. A /\ y = B ) -> y = B )
9	7 8	jca	|- ( ( x e. A /\ y = B ) -> ( x e. C /\ y = B ) )
10	1	ssrab2f	|- { x e. A | B e. _V } C_ A
11	2 10	eqsstri	|- C C_ A
12	11	sseli	|- ( x e. C -> x e. A )
13	12	anim1i	|- ( ( x e. C /\ y = B ) -> ( x e. A /\ y = B ) )
14	9 13	impbii	|- ( ( x e. A /\ y = B ) <-> ( x e. C /\ y = B ) )
15	14	opabbii	|- { <. x , y >. | ( x e. A /\ y = B ) } = { <. x , y >. | ( x e. C /\ y = B ) }
16		df-mpt	|- ( x e. A |-> B ) = { <. x , y >. | ( x e. A /\ y = B ) }
17		df-mpt	|- ( x e. C |-> B ) = { <. x , y >. | ( x e. C /\ y = B ) }
18	15 16 17	3eqtr4i	|- ( x e. A |-> B ) = ( x e. C |-> B )