Theorem ixpeq2dva 7504

Description: Equality theorem for infinite Cartesian product. (Contributed by Mario Carneiro, 11-Jun-2016.)

Hypothesis

Ref	Expression
ixpeq2dva.1

Assertion

Ref	Expression
ixpeq2dva

Distinct variable group:   ,

Proof of Theorem ixpeq2dva

Step	Hyp	Ref	Expression
1		ixpeq2dva.1	. . 3
2	1	ralrimiva 2871	. 2
3		ixpeq2 7503	. 2
4	2, 3	syl 16	1

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

This theorem is referenced by:  ixpeq2dv  7505  dfac9  8537  xpsfrn2  14967  xpslem  14970  funcpropd  15269  natpropd  15345  prdsmgp  17259  frlmip  18809  elptr2  20075  dfac14  20119  xkoptsub  20155  prdsxmslem2  21032  rrxip  21822  ptrest  30048  prdsbnd2  30291

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