Theorem ixpeq1d 7501

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

Hypothesis

Ref	Expression
ixpeq1d.1

Assertion

Ref	Expression
ixpeq1d

Distinct variable groups:   ,   ,

Proof of Theorem ixpeq1d

Step	Hyp	Ref	Expression
1		ixpeq1d.1	. 2
2		ixpeq1 7500	. 2
3	1, 2	syl 16	1

Syntax hints:  ->wi 4  =wceq 1395  X_cixp 7489

This theorem is referenced by:  elixpsn  7528  ixpsnf1o  7529  dfac9  8537  prdsval  14852  isfunc  15233  funcpropd  15269  natfval  15315  natpropd  15345  dprdval  17034  dprdvalOLD  17036  ptval  20071  dfac14  20119  ptuncnv  20308  ptunhmeo  20309

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-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-fn 5596  df-ixp 7490