Theorem resmpt2 6758

Description: Restriction of the mapping operation. (Contributed by Mario Carneiro, 17-Dec-2013.)

Assertion

Ref	Expression
resmpt2	|- ( ( C C_ A /\ D C_ B ) -> ( ( x e. A , y e. B |-> E ) |` ( C X. D ) ) = ( x e. C , y e. D |-> E ) )

Distinct variable groups:   x, A, y   x, B, y   x, C, y   x, D, y

Allowed substitution hints:   E( x, y)

Proof of Theorem resmpt2

Dummy variable z is distinct from all other variables.

Step	Hyp	Ref	Expression
1		resoprab2 6757	. 2 |- ( ( C C_ A /\ D C_ B ) -> ( { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = E ) } |` ( C X. D ) ) = { <. <. x , y >. , z >. | ( ( x e. C /\ y e. D ) /\ z = E ) } )
2		df-mpt2 6655	. . 3 |- ( x e. A , y e. B |-> E ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = E ) }
3	2	reseq1i 5392	. 2 |- ( ( x e. A , y e. B |-> E ) |` ( C X. D ) ) = ( { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = E ) } |` ( C X. D ) )
4		df-mpt2 6655	. 2 |- ( x e. C , y e. D |-> E ) = { <. <. x , y >. , z >. | ( ( x e. C /\ y e. D ) /\ z = E ) }
5	1, 3, 4	3eqtr4g 2681	1 |- ( ( C C_ A /\ D C_ B ) -> ( ( x e. A , y e. B |-> E ) |` ( C X. D ) ) = ( x e. C , y e. D |-> E ) )

Syntax hints:   -> wi 4   /\ wa 384   = wceq 1483   e. wcel 1990   C_ wss 3574   X. cxp 5112   |` cres 5116   {coprab 6651   |-> cmpt2 6652

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-opab 4713  df-xp 5120  df-rel 5121  df-res 5126  df-oprab 6654  df-mpt2 6655

This theorem is referenced by:  ofmres  7164  cantnfval2  8566  pgrpsubgsymg  17828  sylow3lem5  18046  phssip  20003  mamures  20196  mdetrsca2  20410  mdetrlin2  20413  mdetunilem5  20422  smadiadetglem1  20477  smadiadetglem2  20478  pmatcollpw3lem  20588  txss12  21408  txbasval  21409  cnmpt2res  21480  fmucndlem  22095  cnmpt2pc  22727  oprpiece1res1  22750  oprpiece1res2  22751  cxpcn3  24489  ressplusf  29650  submatres  29872  cvmlift2lem6  31290  cvmlift2lem12  31296  icorempt2  33199  elicores  39760  volicorescl  40767  rngchomrnghmresALTV  41996  rhmsubclem1  42086  rhmsubcALTVlem1  42104