Theorem sqxpeqd 5141

Description: Equality deduction for a Cartesian square, see Wikipedia "Cartesian product", https://en.wikipedia.org/wiki/Cartesian_product#n-ary_Cartesian_power. (Contributed by AV, 13-Jan-2020.)

Hypothesis

Ref	Expression
xpeq1d.1	|- ( ph -> A = B )

Assertion

Ref	Expression
sqxpeqd	|- ( ph -> ( A X. A ) = ( B X. B ) )

Proof of Theorem sqxpeqd

Step	Hyp	Ref	Expression
1		xpeq1d.1	. 2 |- ( ph -> A = B )
2	1, 1	xpeq12d 5140	1 |- ( ph -> ( A X. A ) = ( B X. B ) )

Syntax hints:   -> wi 4   = wceq 1483   X. cxp 5112

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

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-opab 4713  df-xp 5120

This theorem is referenced by:  xpcoid  5676  hartogslem1  8447  isfin6  9122  fpwwe2cbv  9452  fpwwe2lem2  9454  fpwwe2lem3  9455  fpwwe2lem8  9459  fpwwe2lem12  9463  fpwwe2lem13  9464  fpwwe2  9465  fpwwecbv  9466  fpwwelem  9467  canthwelem  9472  canthwe  9473  pwfseqlem4  9484  prdsval  16115  imasval  16171  imasaddfnlem  16188  comfffval  16358  comfeq  16366  oppcval  16373  sscfn1  16477  sscfn2  16478  isssc  16480  ssceq  16486  reschomf  16491  isfunc  16524  idfuval  16536  funcres  16556  funcpropd  16560  fucval  16618  fucpropd  16637  homafval  16679  setcval  16727  catcval  16746  estrcval  16764  estrchomfeqhom  16776  hofval  16892  hofpropd  16907  islat  17047  istsr  17217  cnvtsr  17222  isdir  17232  tsrdir  17238  intopsn  17253  frmdval  17388  resgrpplusfrn  17436  opsrval  19474  matval  20217  ustval  22006  trust  22033  utop2nei  22054  utop3cls  22055  utopreg  22056  ussval  22063  ressuss  22067  tususs  22074  fmucnd  22096  cfilufg  22097  trcfilu  22098  neipcfilu  22100  ispsmet  22109  prdsdsf  22172  prdsxmet  22174  ressprdsds  22176  xpsdsfn2  22183  xpsxmetlem  22184  xpsmet  22187  isxms  22252  isms  22254  xmspropd  22278  mspropd  22279  setsxms  22284  setsms  22285  imasf1oxms  22294  imasf1oms  22295  ressxms  22330  ressms  22331  prdsxmslem2  22334  metuval  22354  nmpropd2  22399  ngppropd  22441  tngngp2  22456  pi1addf  22847  pi1addval  22848  iscms  23142  cmspropd  23146  cmsss  23147  rrxds  23181  rrxmfval  23189  minveclem3a  23198  dvlip2  23758  dchrval  24959  brcgr  25780  issh  28065  qtophaus  29903  prsssdm  29963  ordtrestNEW  29967  ordtrest2NEW  29969  isrrext  30044  sibfof  30402  mdvval  31401  msrval  31435  mthmpps  31479  madeval  31935  funtransport  32138  fvtransport  32139  bj-diagval  33090  prdsbnd2  33594  cnpwstotbnd  33596  isrngo  33696  isrngod  33697  rngosn3  33723  isdivrngo  33749  drngoi  33750  isgrpda  33754  ldualset  34412  aomclem8  37631  intopval  41838  rngcvalALTV  41961  rngcval  41962  rnghmsubcsetclem1  41975  rngccat  41978  rngchomrnghmresALTV  41996  ringcvalALTV  42007  ringcval  42008  rhmsubcsetclem1  42021  ringccat  42024  rhmsubcrngclem1  42027  rhmsubcrngc  42029  srhmsubc  42076  rhmsubc  42090  srhmsubcALTV  42094  elpglem3  42456