Theorem f1oeq23 6834

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

Assertion

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

Proof of Theorem f1oeq23

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570  ⟶1-1ontowf1o 6554

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-ss 3901  df-fn 6558  df-f 6559  df-f1 6560  df-fo 6561  df-f1o 6562

This theorem is used by:  f1ofvswap  7334  enfixsn  9130  ackbij2lem2  10341  seqf1o  14210  eulerthlem2  16985  isgim  19502  islmim  21364  fpwrelmapffs  33393  wrdpmcl  33572  1arithidomlem2  34135  1arithidom  34136  hgt750lemg  35350  poimirlem3  38732  poimirlem15  38744  eldioph2lem1  43962  fundcmpsurbijinj  48695  gricushgr  49218  isgrlim  49283