MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  f1oen3g Structured version   Visualization version   GIF version

Theorem f1oen3g 8380
Description: The domain and range of a one-to-one, onto function are equinumerous. This variation of f1oeng 8383 does not require the Axiom of Replacement. (Contributed by NM, 13-Jan-2007.) (Revised by Mario Carneiro, 10-Sep-2015.)
Assertion
Ref Expression
f1oen3g ((𝐹𝑉𝐹:𝐴1-1-onto𝐵) → 𝐴𝐵)

Proof of Theorem f1oen3g
Dummy variable 𝑓 is distinct from all other variables.
StepHypRef Expression
1 f1oeq1 6479 . . . 4 (𝑓 = 𝐹 → (𝑓:𝐴1-1-onto𝐵𝐹:𝐴1-1-onto𝐵))
21spcegv 3542 . . 3 (𝐹𝑉 → (𝐹:𝐴1-1-onto𝐵 → ∃𝑓 𝑓:𝐴1-1-onto𝐵))
32imp 407 . 2 ((𝐹𝑉𝐹:𝐴1-1-onto𝐵) → ∃𝑓 𝑓:𝐴1-1-onto𝐵)
4 bren 8373 . 2 (𝐴𝐵 ↔ ∃𝑓 𝑓:𝐴1-1-onto𝐵)
53, 4sylibr 235 1 ((𝐹𝑉𝐹:𝐴1-1-onto𝐵) → 𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wex 1765  wcel 2083   class class class wbr 4968  1-1-ontowf1o 6231  cen 8361
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-13 2346  ax-ext 2771  ax-sep 5101  ax-nul 5108  ax-pr 5228  ax-un 7326
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-mo 2578  df-eu 2614  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-ral 3112  df-rex 3113  df-rab 3116  df-v 3442  df-dif 3868  df-un 3870  df-in 3872  df-ss 3880  df-nul 4218  df-if 4388  df-sn 4479  df-pr 4481  df-op 4485  df-uni 4752  df-br 4969  df-opab 5031  df-xp 5456  df-rel 5457  df-cnv 5458  df-co 5459  df-dm 5460  df-rn 5461  df-fun 6234  df-fn 6235  df-f 6236  df-f1 6237  df-fo 6238  df-f1o 6239  df-en 8365
This theorem is referenced by:  f1oen2g  8381  unen  8451  domdifsn  8454  domunsncan  8471  sbthlem10  8490  domssex  8532  phplem2  8551  sucdom2  8567  pssnn  8589  f1finf1o  8598  oien  8855  infdifsn  8973  fin4en1  9584  fin23lem21  9614  hashf1lem2  13666  odinf  18424  gsumval3lem2  18751  gsumval3  18752  hmphen2  22095  fnpreimac  30102  pibt2  34250
  Copyright terms: Public domain W3C validator