Theorem f1oeq23 6794

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 6792	. 2 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐹:𝐵–1-1-onto→𝐶))
2		f1oeq3 6793	. 2 ⊢ (𝐶 = 𝐷 → (𝐹:𝐵–1-1-onto→𝐶 ↔ 𝐹:𝐵–1-1-onto→𝐷))
3	1, 2	sylan9bb 509	1 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐹:𝐵–1-1-onto→𝐷))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540  –1-1-onto→wf1o 6513

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-ss 3934  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521

This theorem is referenced by:  f1ofvswap  7284  enfixsn  9055  ackbij2lem2  10199  seqf1o  14015  eulerthlem2  16759  isgim  19201  islmim  20976  fpwrelmapffs  32664  wrdpmcl  32866  1arithidomlem2  33514  1arithidom  33515  hgt750lemg  34652  poimirlem3  37624  poimirlem15  37636  eldioph2lem1  42755  fundcmpsurbijinj  47415  gricushgr  47921  isgrlim  47985