Theorem f1oeq2 5061

Description: Equality theorem for one-to-one onto functions. (Contributed by NM, 10-Feb-1997.)

Assertion

Ref	Expression
f1oeq2	⊢ (A = B → (𝐹:A–1-1-onto→𝐶 ↔ 𝐹:B–1-1-onto→𝐶))

Proof of Theorem f1oeq2

Step	Hyp	Ref	Expression
1		f1eq2 5031	. . 3 ⊢ (A = B → (𝐹:A–1-1→𝐶 ↔ 𝐹:B–1-1→𝐶))
2		foeq2 5046	. . 3 ⊢ (A = B → (𝐹:A–onto→𝐶 ↔ 𝐹:B–onto→𝐶))
3	1, 2	anbi12d 442	. 2 ⊢ (A = B → ((𝐹:A–1-1→𝐶 ∧ 𝐹:A–onto→𝐶) ↔ (𝐹:B–1-1→𝐶 ∧ 𝐹:B–onto→𝐶)))
4		df-f1o 4852	. 2 ⊢ (𝐹:A–1-1-onto→𝐶 ↔ (𝐹:A–1-1→𝐶 ∧ 𝐹:A–onto→𝐶))
5		df-f1o 4852	. 2 ⊢ (𝐹:B–1-1-onto→𝐶 ↔ (𝐹:B–1-1→𝐶 ∧ 𝐹:B–onto→𝐶))
6	3, 4, 5	3bitr4g 212	1 ⊢ (A = B → (𝐹:A–1-1-onto→𝐶 ↔ 𝐹:B–1-1-onto→𝐶))

Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98   = wceq 1242  –1-1→wf1 4842  –onto→wfo 4843  –1-1-onto→wf1o 4844

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-gen 1335  ax-4 1397  ax-17 1416  ax-ext 2019

This theorem depends on definitions:  df-bi 110  df-cleq 2030  df-fn 4848  df-f 4849  df-f1 4850  df-fo 4851  df-f1o 4852

This theorem is referenced by:  f1oeq23  5063  f1oeq123d  5066  f1osng  5110  isoeq4  5387  bren  6164