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  25941  erdszelem1  35171  erdsze  35182  erdsze2lem1  35183  erdsze2lem2  35184  isoeq145d  43401  alephiso3  43541  fourierdlem50  46147  fourierdlem89  46186  fourierdlem90  46187  fourierdlem91  46188  fourierdlem96  46193  fourierdlem97  46194  fourierdlem98  46195  fourierdlem99  46196  fourierdlem100  46197  fourierdlem108  46205  fourierdlem110  46207  fourierdlem112  46209  fourierdlem113  46210