Theorem f1oeq23 6816

Description: Equality theorem for one-to-one onto functions. (Contributed by FL, 14-Jul-2012.)

Assertion

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

Proof of Theorem f1oeq23

Step	Hyp	Ref	Expression
1		f1oeq2 6814	. 2 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐹:𝐵–1-1-onto→𝐶))
2		f1oeq3 6815	. 2 ⊢ (𝐶 = 𝐷 → (𝐹:𝐵–1-1-onto→𝐶 ↔ 𝐹:𝐵–1-1-onto→𝐷))
3	1, 2	sylan9bb 519	1 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐹:𝐵–1-1-onto→𝐷))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570  –1-1-onto→wf1o 6540

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757  df-ss 3923  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548

This theorem is used by:  f1ofvswap  7314  enfixsn  9082  ackbij2lem2  10239  seqf1o  14102  eulerthlem2  16868  isgim  19381  islmim  21238  fpwrelmapffs  33154  wrdpmcl  33333  1arithidomlem2  33895  1arithidom  33896  hgt750lemg  35111  poimirlem3  38336  poimirlem15  38348  eldioph2lem1  43569  fundcmpsurbijinj  48237  gricushgr  48760  isgrlim  48825