Theorem ixpeq2dv 7924

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

Hypothesis

Ref	Expression
ixpeq2dv.1	|- ( ph -> B = C )

Assertion

Ref	Expression
ixpeq2dv	|- ( ph -> X_ x e. A B = X_ x e. A C )

Distinct variable group:   ph, x

Allowed substitution hints:   A( x)   B( x)   C( x)

Proof of Theorem ixpeq2dv

Step	Hyp	Ref	Expression
1		ixpeq2dv.1	. . 3 |- ( ph -> B = C )
2	1	adantr 481	. 2 |- ( ( ph /\ x e. A ) -> B = C )
3	2	ixpeq2dva 7923	1 |- ( ph -> X_ x e. A B = X_ x e. A C )

Syntax hints:   -> wi 4   = wceq 1483   e. wcel 1990   X_cixp 7908

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-nfc 2753  df-ral 2917  df-in 3581  df-ss 3588  df-ixp 7909

This theorem is referenced by:  prdsval  16115  brssc  16474  isfunc  16524  natfval  16606  isnat  16607  dprdval  18402  elpt  21375  elptr  21376  dfac14  21421  hoicvrrex  40770  ovncvrrp  40778  ovnsubaddlem1  40784  ovnsubadd  40786  hoidmvlelem3  40811  hoidmvle  40814  ovnhoilem1  40815  ovnhoilem2  40816  ovnhoi  40817  hspval  40823  ovncvr2  40825  hspmbllem2  40841  hspmbl  40843  hoimbl  40845  opnvonmbl  40848  ovnovollem1  40870  ovnovollem3  40872  iinhoiicclem  40887  iinhoiicc  40888  vonioolem2  40895  vonioo  40896  vonicclem2  40898  vonicc  40899