Theorem isoeq1 7261

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

Assertion

Ref	Expression
isoeq1	⊢ (𝐻 = 𝐺 → (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐺 Isom 𝑅, 𝑆 (𝐴, 𝐵)))

Proof of Theorem isoeq1

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

Step	Hyp	Ref	Expression
1		f1oeq1 6755	. . 3 ⊢ (𝐻 = 𝐺 → (𝐻:𝐴–1-1-onto→𝐵 ↔ 𝐺:𝐴–1-1-onto→𝐵))
2		fveq1 6826	. . . . . 6 ⊢ (𝐻 = 𝐺 → (𝐻‘𝑥) = (𝐺‘𝑥))
3		fveq1 6826	. . . . . 6 ⊢ (𝐻 = 𝐺 → (𝐻‘𝑦) = (𝐺‘𝑦))
4	2, 3	breq12d 5085	. . . . 5 ⊢ (𝐻 = 𝐺 → ((𝐻‘𝑥)𝑆(𝐻‘𝑦) ↔ (𝐺‘𝑥)𝑆(𝐺‘𝑦)))
5	4	bibi2d 343	. . . 4 ⊢ (𝐻 = 𝐺 → ((𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)) ↔ (𝑥𝑅𝑦 ↔ (𝐺‘𝑥)𝑆(𝐺‘𝑦))))
6	5	2ralbidv 3203	. . 3 ⊢ (𝐻 = 𝐺 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐺‘𝑥)𝑆(𝐺‘𝑦))))
7	1, 6	anbi12d 638	. 2 ⊢ (𝐻 = 𝐺 → ((𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))) ↔ (𝐺:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐺‘𝑥)𝑆(𝐺‘𝑦)))))
8		df-isom 6494	. 2 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))))
9		df-isom 6494	. 2 ⊢ (𝐺 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐺:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐺‘𝑥)𝑆(𝐺‘𝑦))))
10	7, 8, 9	3bitr4g 315	1 ⊢ (𝐻 = 𝐺 → (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐺 Isom 𝑅, 𝑆 (𝐴, 𝐵)))

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1547  ∀wral 3053   class class class wbr 5072  –1-1-onto→wf1o 6484  ‘cfv 6485   Isom wiso 6486

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ral 3054  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-isom 6494

This theorem is referenced by:  isores1  7278  wemoiso  7915  wemoiso2  7916  ordiso  9421  oieu  9444  finnisoeu  10026  iunfictbso  10027  infrenegsup  12130  ltweuz  13914  fz1isolem  14414  isercolllem2  15619  isercoll  15621  dvgt0lem2  25988  efcvx  26432  relogiso  26580  logccv  26645  erdszelem1  35419  erdsze  35430  erdsze2lem2  35432  isoeq145d  43863  fzisoeu  45748  fourierdlem36  46586  fourierdlem96  46645  fourierdlem97  46646  fourierdlem98  46647  fourierdlem99  46648  fourierdlem105  46654  fourierdlem106  46655  fourierdlem108  46657  fourierdlem110  46659  fourierdlem112  46661  fourierdlem113  46662  fourierdlem115  46664  rrx2plordisom  49214