Theorem isoeq5 7276

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 6770	. . 3 ⊢ (𝐵 = 𝐶 → (𝐻:𝐴–1-1-onto→𝐵 ↔ 𝐻:𝐴–1-1-onto→𝐶))
2	1	anbi1d 632	. 2 ⊢ (𝐵 = 𝐶 → ((𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))) ↔ (𝐻:𝐴–1-1-onto→𝐶 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)))))
3		df-isom 6507	. 2 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))))
4		df-isom 6507	. 2 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐶) ↔ (𝐻:𝐴–1-1-onto→𝐶 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))))
5	2, 3, 4	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-ss 3906  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-isom 6507

This theorem is referenced by:  isores3  7290  ordiso  9431  ordtypelem9  9441  ordtypelem10  9442  oiid  9456  iunfictbso  10036  ltweuz  13923  fz1isolem  14423  dvgt0lem2  25970  erdszelem1  35373  erdsze  35384  erdsze2lem1  35385  erdsze2lem2  35386  isoeq145d  43846  alephiso3  43986  fourierdlem50  46584  fourierdlem89  46623  fourierdlem90  46624  fourierdlem91  46625  fourierdlem96  46630  fourierdlem97  46631  fourierdlem98  46632  fourierdlem99  46633  fourierdlem100  46634  fourierdlem108  46642  fourierdlem110  46644  fourierdlem112  46646  fourierdlem113  46647