Theorem ixpeq2 7503

Description: Equality theorem for infinite Cartesian product. (Contributed by NM, 29-Sep-2006.)

Assertion

Ref	Expression
ixpeq2

Proof of Theorem ixpeq2

Step	Hyp	Ref	Expression
1		ss2ixp 7502	. . 3
2		ss2ixp 7502	. . 3
3	1, 2	anim12i 566	. 2
4		eqss 3518	. . . 4
5	4	ralbii 2888	. . 3
6		r19.26 2984	. . 3
7	5, 6	bitri 249	. 2
8		eqss 3518	. 2
9	3, 7, 8	3imtr4i 266	1

Syntax hints:  ->wi 4  /\wa 369  =wceq 1395  A.wral 2807  C_wss 3475  X_cixp 7489

This theorem is referenced by:  ixpeq2dva  7504  ixpint  7516  prdsbas3  14878  pwsbas  14884  ptbasfi  20082  ptunimpt  20096  pttopon  20097  ptcld  20114  ptrescn  20140  ptuncnv  20308  ptunhmeo  20309  ptrest  30048  prdstotbnd  30290

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812  df-in 3482  df-ss 3489  df-ixp 7490