Theorem ixpeq1 8856

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 6590	. . . 4 ⊢ (𝐴 = 𝐵 → (𝑓 Fn 𝐴 ↔ 𝑓 Fn 𝐵))
2		raleq 3292	. . . 4 ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐶 ↔ ∀𝑥 ∈ 𝐵 (𝑓‘𝑥) ∈ 𝐶))
3	1, 2	anbi12d 633	. . 3 ⊢ (𝐴 = 𝐵 → ((𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐶) ↔ (𝑓 Fn 𝐵 ∧ ∀𝑥 ∈ 𝐵 (𝑓‘𝑥) ∈ 𝐶)))
4	3	abbidv 2802	. 2 ⊢ (𝐴 = 𝐵 → {𝑓 ∣ (𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐶)} = {𝑓 ∣ (𝑓 Fn 𝐵 ∧ ∀𝑥 ∈ 𝐵 (𝑓‘𝑥) ∈ 𝐶)})
5		dfixp 8847	. 2 ⊢ X𝑥 ∈ 𝐴 𝐶 = {𝑓 ∣ (𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐶)}
6		dfixp 8847	. 2 ⊢ X𝑥 ∈ 𝐵 𝐶 = {𝑓 ∣ (𝑓 Fn 𝐵 ∧ ∀𝑥 ∈ 𝐵 (𝑓‘𝑥) ∈ 𝐶)}
7	4, 5, 6	3eqtr4g 2796	1 ⊢ (𝐴 = 𝐵 → X𝑥 ∈ 𝐴 𝐶 = X𝑥 ∈ 𝐵 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  {cab 2714  ∀wral 3051   Fn wfn 6493  ‘cfv 6498  Xcixp 8845

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3062  df-fn 6501  df-ixp 8846

This theorem is referenced by:  ixpeq1d  8857  finixpnum  37926  ioorrnopn  46733  ioorrnopnxr  46735  ovnval  46969  hoicvr  46976  hoidmv1le  47022  hoidmvle  47028  ovnhoi  47031  hspval  47037  ovnlecvr2  47038  hoiqssbl  47053  vonhoire  47100  iunhoiioo  47104  vonioo  47110  vonicc  47113