Theorem f1oeq23 6818

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 6816	. 2 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐹:𝐵–1-1-onto→𝐶))
2		f1oeq3 6817	. 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 6542

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 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2758  df-ss 3925  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550

This theorem is used by:  f1ofvswap  7315  enfixsn  9084  ackbij2lem2  10241  seqf1o  14099  eulerthlem2  16866  isgim  19363  islmim  21220  fpwrelmapffs  33116  wrdpmcl  33295  1arithidomlem2  33857  1arithidom  33858  hgt750lemg  35072  poimirlem3  38314  poimirlem15  38326  eldioph2lem1  43531  fundcmpsurbijinj  48199  gricushgr  48722  isgrlim  48787