Theorem dff1o3 6388

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 1122	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵) ↔ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) ∧ Fun ◡𝐹))
2		dff1o2 6387	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵))
3		df-fo 6133	. . 3 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
4	3	anbi1i 617	. 2 ⊢ ((𝐹:𝐴–onto→𝐵 ∧ Fun ◡𝐹) ↔ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) ∧ Fun ◡𝐹))
5	1, 2, 4	3bitr4i 295	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–onto→𝐵 ∧ Fun ◡𝐹))

Syntax hints:   ↔ wb 198   ∧ wa 386   ∧ w3a 1111   = wceq 1656  ^◡ccnv 5345  ran crn 5347  Fun wfun 6121   Fn wfn 6122  –onto→wfo 6125  –1-1-onto→wf1o 6126

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3an 1113  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-clab 2812  df-cleq 2818  df-clel 2821  df-in 3805  df-ss 3812  df-f 6131  df-f1 6132  df-fo 6133  df-f1o 6134

This theorem is referenced by:  f1ofo  6389  resdif  6402  f1opw  7154  f11o  7395  1stconst  7534  2ndconst  7535  curry1  7538  curry2  7541  f1o2ndf1  7554  ssdomg  8274  phplem4  8417  php3  8421  f1opwfi  8545  cantnfp1lem3  8861  fpwwe2lem6  9779  canthp1lem2  9797  odf1o2  18346  dprdf1o  18792  relogf1o  24719  iseupthf1o  27574  padct  30041  ballotlemfrc  31130  poimirlem1  33953  poimirlem2  33954  poimirlem3  33955  poimirlem4  33956  poimirlem6  33958  poimirlem7  33959  poimirlem9  33961  poimirlem11  33963  poimirlem12  33964  poimirlem13  33965  poimirlem14  33966  poimirlem16  33968  poimirlem17  33969  poimirlem19  33971  poimirlem20  33972  poimirlem23  33975  poimirlem24  33976  poimirlem25  33977  poimirlem29  33981  poimirlem31  33983  ntrneifv2  39217