Theorem ixpeq1 8902

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

Assertion

Ref	Expression
ixpeq1	⊢ (𝐴 = 𝐵 → X𝑥 ∈ 𝐴 𝐶 = X𝑥 ∈ 𝐵 𝐶)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Allowed substitution hint:   𝐶(𝑥)

Proof of Theorem ixpeq1

Dummy variable 𝑓 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		fneq2 6642	. . . 4 ⊢ (𝐴 = 𝐵 → (𝑓 Fn 𝐴 ↔ 𝑓 Fn 𝐵))
2		raleq 3323	. . . 4 ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐶 ↔ ∀𝑥 ∈ 𝐵 (𝑓‘𝑥) ∈ 𝐶))
3	1, 2	anbi12d 632	. . 3 ⊢ (𝐴 = 𝐵 → ((𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐶) ↔ (𝑓 Fn 𝐵 ∧ ∀𝑥 ∈ 𝐵 (𝑓‘𝑥) ∈ 𝐶)))
4	3	abbidv 2802	. 2 ⊢ (𝐴 = 𝐵 → {𝑓 ∣ (𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐶)} = {𝑓 ∣ (𝑓 Fn 𝐵 ∧ ∀𝑥 ∈ 𝐵 (𝑓‘𝑥) ∈ 𝐶)})
5		dfixp 8893	. 2 ⊢ X𝑥 ∈ 𝐴 𝐶 = {𝑓 ∣ (𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐶)}
6		dfixp 8893	. 2 ⊢ X𝑥 ∈ 𝐵 𝐶 = {𝑓 ∣ (𝑓 Fn 𝐵 ∧ ∀𝑥 ∈ 𝐵 (𝑓‘𝑥) ∈ 𝐶)}
7	4, 5, 6	3eqtr4g 2798	1 ⊢ (𝐴 = 𝐵 → X𝑥 ∈ 𝐴 𝐶 = X𝑥 ∈ 𝐵 𝐶)

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1542   ∈ wcel 2107  {cab 2710  ∀wral 3062   Fn wfn 6539  ‘cfv 6544  Xcixp 8891

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rex 3072  df-fn 6547  df-ixp 8892

This theorem is referenced by:  ixpeq1d  8903  finixpnum  36473  ioorrnopn  45021  ioorrnopnxr  45023  ovnval  45257  hoicvr  45264  hoidmv1le  45310  hoidmvle  45316  ovnhoi  45319  hspval  45325  ovnlecvr2  45326  hoiqssbl  45341  vonhoire  45388  iunhoiioo  45392  vonioo  45398  vonicc  45401