Theorem f1oeq3 5511

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

Assertion

Ref	Expression
f1oeq3	⊢ (𝐴 = 𝐵 → (𝐹:𝐶–1-1-onto→𝐴 ↔ 𝐹:𝐶–1-1-onto→𝐵))

Proof of Theorem f1oeq3

Step	Hyp	Ref	Expression
1		f1eq3 5477	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–1-1→𝐴 ↔ 𝐹:𝐶–1-1→𝐵))
2		foeq3 5495	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–onto→𝐴 ↔ 𝐹:𝐶–onto→𝐵))
3	1, 2	anbi12d 473	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴) ↔ (𝐹:𝐶–1-1→𝐵 ∧ 𝐹:𝐶–onto→𝐵)))
4		df-f1o 5277	. 2 ⊢ (𝐹:𝐶–1-1-onto→𝐴 ↔ (𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴))
5		df-f1o 5277	. 2 ⊢ (𝐹:𝐶–1-1-onto→𝐵 ↔ (𝐹:𝐶–1-1→𝐵 ∧ 𝐹:𝐶–onto→𝐵))
6	3, 4, 5	3bitr4g 223	1 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–1-1-onto→𝐴 ↔ 𝐹:𝐶–1-1-onto→𝐵))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1372  –1-1→wf1 5267  –onto→wfo 5268  –1-1-onto→wf1o 5269

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-11 1528  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-in 3171  df-ss 3178  df-f 5274  df-f1 5275  df-fo 5276  df-f1o 5277

This theorem is referenced by:  f1oeq23  5512  f1oeq123d  5515  f1oeq3d  5518  f1ores  5536  resdif  5543  f1osng  5562  f1oresrab  5744  isoeq5  5873  isoini2  5887  mapsnf1o  6823  breng  6833  bren  6834  xpcomf1o  6919  frechashgf1o  10571  sumeq1  11637  fisumss  11674  fsumcnv  11719  prodeq1f  11834  4sqlem11  12695  ennnfonelemhf1o  12755  ennnfonelemex  12756  ssnnctlemct  12788