Theorem isoeq4 7275

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 6769	. . 3 ⊢ (𝐴 = 𝐶 → (𝐻:𝐴–1-1-onto→𝐵 ↔ 𝐻:𝐶–1-1-onto→𝐵))
2		raleq 3292	. . . 4 ⊢ (𝐴 = 𝐶 → (∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)) ↔ ∀𝑦 ∈ 𝐶 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))))
3	2	raleqbi1dv 3305	. . 3 ⊢ (𝐴 = 𝐶 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)) ↔ ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐶 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))))
4	1, 3	anbi12d 633	. 2 ⊢ (𝐴 = 𝐶 → ((𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))) ↔ (𝐻:𝐶–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐶 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)))))
5		df-isom 6507	. 2 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))))
6		df-isom 6507	. 2 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐶, 𝐵) ↔ (𝐻:𝐶–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐶 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))))
7	4, 5, 6	3bitr4g 314	1 ⊢ (𝐴 = 𝐶 → (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐻 Isom 𝑅, 𝑆 (𝐶, 𝐵)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542  ∀wral 3051   class class class wbr 5085  –1-1-onto→wf1o 6497  ‘cfv 6498   Isom wiso 6499

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-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-ral 3052  df-rex 3062  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-isom 6507

This theorem is referenced by:  oieu  9454  oiid  9456  finnisoeu  10035  iunfictbso  10036  fz1isolem  14423  isercolllem3  15629  summolem2a  15677  prodmolem2a  15899  erdszelem1  35373  erdsze  35384  erdsze2lem1  35385  erdsze2lem2  35386  isoeq145d  43846  fzisoeu  45733  fourierdlem36  46571  fourierdlem112  46646  fourierdlem113  46647