Theorem f1oeq23 6763

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 6761	. 2 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐹:𝐵–1-1-onto→𝐶))
2		f1oeq3 6762	. 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 1541  –1-1-onto→wf1o 6489

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2726  df-ss 3916  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497

This theorem is referenced by:  f1ofvswap  7250  enfixsn  9012  ackbij2lem2  10147  seqf1o  13964  eulerthlem2  16707  isgim  19189  islmim  21012  fpwrelmapffs  32762  wrdpmcl  32969  1arithidomlem2  33566  1arithidom  33567  hgt750lemg  34760  poimirlem3  37763  poimirlem15  37775  eldioph2lem1  42944  fundcmpsurbijinj  47598  gricushgr  48105  isgrlim  48170