Theorem f1oeq23 6799

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   = wceq 1562  –1-1-onto→wf1o 6522

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1802  df-cleq 2756  df-ss 3923  df-fn 6526  df-f 6527  df-f1 6528  df-fo 6529  df-f1o 6530

This theorem is referenced by:  f1ofvswap  7292  enfixsn  9060  ackbij2lem2  10197  seqf1o  14058  eulerthlem2  16819  isgim  19304  islmim  21131  fpwrelmapffs  32938  wrdpmcl  33118  1arithidomlem2  33734  1arithidom  33735  hgt750lemg  34950  poimirlem3  38127  poimirlem15  38139  eldioph2lem1  43346  fundcmpsurbijinj  48021  gricushgr  48544  isgrlim  48609