Theorem dff1o3 6831

Description: Alternate definition of one-to-one onto function. (Contributed by NM, 25-Mar-1998.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)

Assertion

Ref	Expression
dff1o3	⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–onto→𝐵 ∧ Fun ◡𝐹))

Proof of Theorem dff1o3

Step	Hyp	Ref	Expression
1		3anan32 1113	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵) ↔ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) ∧ Fun ◡𝐹))
2		dff1o2 6830	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵))
3		df-fo 6546	. . 3 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
4	3	anbi1i 636	. 2 ⊢ ((𝐹:𝐴–onto→𝐵 ∧ Fun ◡𝐹) ↔ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) ∧ Fun ◡𝐹))
5	1, 2, 4	3bitr4i 306	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–onto→𝐵 ∧ Fun ◡𝐹))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570  ^◡ccnv 5662  ran crn 5664  Fun wfun 6534   Fn wfn 6535  –onto→wfo 6538  –1-1-onto→wf1o 6539

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 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-ex 1813  df-cleq 2757  df-ss 3923  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547

This theorem is used by:  f1ofo  6832  resdif  6846  f1opw  7672  f11o  7946  1stconst  8097  2ndconst  8098  curry1  8101  curry2  8104  f1o2ndf1  8119  ssdomg  8999  dif1enlem  9147  phplem2  9192  php3  9196  f1opwfi  9316  cantnfp1lem3  9652  fpwwe2lem5  10631  canthp1lem2  10649  odf1o2  19667  dprdf1o  20128  relogf1o  26762  iseupthf1o  30600  padct  33109  ballotlemfrc  34958  poimirlem1  38305  poimirlem2  38306  poimirlem3  38307  poimirlem4  38308  poimirlem6  38310  poimirlem7  38311  poimirlem9  38313  poimirlem11  38315  poimirlem12  38316  poimirlem13  38317  poimirlem14  38318  poimirlem16  38320  poimirlem17  38321  poimirlem19  38323  poimirlem20  38324  poimirlem23  38327  poimirlem24  38328  poimirlem25  38329  poimirlem29  38333  poimirlem31  38335  ntrneifv2  44839  permaxpow  45751  upgrimpthslem1  48705  upgrimspths  48708  idfth  49969  idsubc  49971