Theorem isoeq5 7270

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 6765	. . 3 ⊢ (𝐵 = 𝐶 → (𝐻:𝐴–1-1-onto→𝐵 ↔ 𝐻:𝐴–1-1-onto→𝐶))
2	1	anbi1d 632	. 2 ⊢ (𝐵 = 𝐶 → ((𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))) ↔ (𝐻:𝐴–1-1-onto→𝐶 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)))))
3		df-isom 6502	. 2 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))))
4		df-isom 6502	. 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 3052   class class class wbr 5086  –1-1-onto→wf1o 6492  ‘cfv 6493   Isom wiso 6494

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ss 3907  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-isom 6502

This theorem is referenced by:  isores3  7284  ordiso  9425  ordtypelem9  9435  ordtypelem10  9436  oiid  9450  iunfictbso  10030  ltweuz  13917  fz1isolem  14417  dvgt0lem2  25983  erdszelem1  35392  erdsze  35403  erdsze2lem1  35404  erdsze2lem2  35405  isoeq145d  43867  alephiso3  44007  fourierdlem50  46605  fourierdlem89  46644  fourierdlem90  46645  fourierdlem91  46646  fourierdlem96  46651  fourierdlem97  46652  fourierdlem98  46653  fourierdlem99  46654  fourierdlem100  46655  fourierdlem108  46663  fourierdlem110  46665  fourierdlem112  46667  fourierdlem113  46668