Theorem dff1o3 6808

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 1107	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵) ↔ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) ∧ Fun ◡𝐹))
2		dff1o2 6807	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵))
3		df-fo 6522	. . 3 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
4	3	anbi1i 633	. 2 ⊢ ((𝐹:𝐴–onto→𝐵 ∧ Fun ◡𝐹) ↔ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) ∧ Fun ◡𝐹))
5	1, 2, 4	3bitr4i 305	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–onto→𝐵 ∧ Fun ◡𝐹))

Syntax hints:   ↔ wb 208   ∧ wa 399   ∧ w3a 1097   = wceq 1559  ^◡ccnv 5642  ran crn 5644  Fun wfun 6510   Fn wfn 6511  –onto→wfo 6514  –1-1-onto→wf1o 6515

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-3an 1099  df-ex 1799  df-cleq 2753  df-ss 3919  df-f 6520  df-f1 6521  df-fo 6522  df-f1o 6523

This theorem is referenced by:  f1ofo  6809  resdif  6823  f1opw  7647  f11o  7923  1stconst  8073  2ndconst  8074  curry1  8077  curry2  8080  f1o2ndf1  8095  ssdomg  8975  dif1enlem  9122  phplem2  9167  php3  9171  f1opwfi  9293  cantnfp1lem3  9629  fpwwe2lem5  10587  canthp1lem2  10605  odf1o2  19604  dprdf1o  20065  relogf1o  26619  iseupthf1o  30361  padct  32881  ballotlemfrc  34785  poimirlem1  38081  poimirlem2  38082  poimirlem3  38083  poimirlem4  38084  poimirlem6  38086  poimirlem7  38087  poimirlem9  38089  poimirlem11  38091  poimirlem12  38092  poimirlem13  38093  poimirlem14  38094  poimirlem16  38096  poimirlem17  38097  poimirlem19  38099  poimirlem20  38100  poimirlem23  38103  poimirlem24  38104  poimirlem25  38105  poimirlem29  38109  poimirlem31  38111  ntrneifv2  44617  permaxpow  45546  upgrimpthslem1  48490  upgrimspths  48493  idfth  49740  idsubc  49742