Theorem dff1o3 6824

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 6823	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵))
3		df-fo 6539	. . 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 5654  ran crn 5656  Fun wfun 6527   Fn wfn 6528  –onto→wfo 6531  –1-1-onto→wf1o 6532

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 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-ex 1813  df-cleq 2752  df-ss 3916  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540

This theorem is used by:  f1ofo  6825  resdif  6839  f1opw  7670  f11o  7944  1stconst  8097  2ndconst  8098  curry1  8101  curry2  8104  f1o2ndf1  8119  ssdomg  9006  dif1enlem  9154  phplem2  9199  php3  9203  f1opwfi  9323  cantnfp1lem3  9659  fpwwe2lem5  10644  canthp1lem2  10662  odf1o2  19700  dprdf1o  20161  relogf1o  26803  iseupthf1o  30682  padct  33189  ballotlemfrc  35038  poimirlem1  38370  poimirlem2  38371  poimirlem3  38372  poimirlem4  38373  poimirlem6  38375  poimirlem7  38376  poimirlem9  38378  poimirlem11  38380  poimirlem12  38381  poimirlem13  38382  poimirlem14  38383  poimirlem16  38385  poimirlem17  38386  poimirlem19  38388  poimirlem20  38389  poimirlem23  38392  poimirlem24  38393  poimirlem25  38394  poimirlem29  38398  poimirlem31  38400  ntrneifv2  44920  permaxpow  45832  upgrimpthslem1  48823  upgrimspths  48826  idfth  50084  idsubc  50086