Theorem isoeq5 7278

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

Assertion

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

Proof of Theorem isoeq5

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

Step	Hyp	Ref	Expression
1		f1oeq3 6772	. . 3 ⊢ (𝐵 = 𝐶 → (𝐻:𝐴–1-1-onto→𝐵 ↔ 𝐻:𝐴–1-1-onto→𝐶))
2	1	anbi1d 631	. 2 ⊢ (𝐵 = 𝐶 → ((𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))) ↔ (𝐻:𝐴–1-1-onto→𝐶 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)))))
3		df-isom 6508	. 2 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))))
4		df-isom 6508	. 2 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐶) ↔ (𝐻:𝐴–1-1-onto→𝐶 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))))
5	2, 3, 4	3bitr4g 314	1 ⊢ (𝐵 = 𝐶 → (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐶)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540  ∀wral 3044   class class class wbr 5102  –1-1-onto→wf1o 6498  ‘cfv 6499   Isom wiso 6500

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ss 3928  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-isom 6508

This theorem is referenced by:  isores3  7292  ordiso  9445  ordtypelem9  9455  ordtypelem10  9456  oiid  9470  iunfictbso  10043  ltweuz  13902  fz1isolem  14402  dvgt0lem2  25884  erdszelem1  35151  erdsze  35162  erdsze2lem1  35163  erdsze2lem2  35164  isoeq145d  43381  alephiso3  43521  fourierdlem50  46127  fourierdlem89  46166  fourierdlem90  46167  fourierdlem91  46168  fourierdlem96  46173  fourierdlem97  46174  fourierdlem98  46175  fourierdlem99  46176  fourierdlem100  46177  fourierdlem108  46185  fourierdlem110  46187  fourierdlem112  46189  fourierdlem113  46190