Theorem isoeq4 7339

Description: Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.)

Assertion

Ref	Expression
isoeq4	⊢ (𝐴 = 𝐶 → (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐻 Isom 𝑅, 𝑆 (𝐶, 𝐵)))

Proof of Theorem isoeq4

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		f1oeq2 6837	. . 3 ⊢ (𝐴 = 𝐶 → (𝐻:𝐴–1-1-onto→𝐵 ↔ 𝐻:𝐶–1-1-onto→𝐵))
2		raleq 3320	. . . 4 ⊢ (𝐴 = 𝐶 → (∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)) ↔ ∀𝑦 ∈ 𝐶 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))))
3	2	raleqbi1dv 3335	. . 3 ⊢ (𝐴 = 𝐶 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)) ↔ ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐶 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))))
4	1, 3	anbi12d 632	. 2 ⊢ (𝐴 = 𝐶 → ((𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))) ↔ (𝐻:𝐶–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐶 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)))))
5		df-isom 6571	. 2 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))))
6		df-isom 6571	. 2 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐶, 𝐵) ↔ (𝐻:𝐶–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐶 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))))
7	4, 5, 6	3bitr4g 314	1 ⊢ (𝐴 = 𝐶 → (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐻 Isom 𝑅, 𝑆 (𝐶, 𝐵)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1536  ∀wral 3058   class class class wbr 5147  –1-1-onto→wf1o 6561  ‘cfv 6562   Isom wiso 6563

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-ral 3059  df-rex 3068  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-isom 6571

This theorem is referenced by:  oieu  9576  oiid  9578  finnisoeu  10150  iunfictbso  10151  fz1isolem  14496  isercolllem3  15699  summolem2a  15747  prodmolem2a  15966  erdszelem1  35175  erdsze  35186  erdsze2lem1  35187  erdsze2lem2  35188  isoeq145d  43408  fzisoeu  45250  fourierdlem36  46098  fourierdlem112  46173  fourierdlem113  46174