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

Theorem f1oen2g 8527
 Description: The domain and range of a one-to-one, onto function are equinumerous. This variation of f1oeng 8529 does not require the Axiom of Replacement. (Contributed by Mario Carneiro, 10-Sep-2015.)
Assertion
Ref Expression
f1oen2g ((𝐴𝑉𝐵𝑊𝐹:𝐴1-1-onto𝐵) → 𝐴𝐵)

Proof of Theorem f1oen2g
StepHypRef Expression
1 f1of 6599 . . . 4 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴𝐵)
2 fex2 7633 . . . 4 ((𝐹:𝐴𝐵𝐴𝑉𝐵𝑊) → 𝐹 ∈ V)
31, 2syl3an1 1160 . . 3 ((𝐹:𝐴1-1-onto𝐵𝐴𝑉𝐵𝑊) → 𝐹 ∈ V)
433coml 1124 . 2 ((𝐴𝑉𝐵𝑊𝐹:𝐴1-1-onto𝐵) → 𝐹 ∈ V)
5 simp3 1135 . 2 ((𝐴𝑉𝐵𝑊𝐹:𝐴1-1-onto𝐵) → 𝐹:𝐴1-1-onto𝐵)
6 f1oen3g 8526 . 2 ((𝐹 ∈ V ∧ 𝐹:𝐴1-1-onto𝐵) → 𝐴𝐵)
74, 5, 6syl2anc 587 1 ((𝐴𝑉𝐵𝑊𝐹:𝐴1-1-onto𝐵) → 𝐴𝐵)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ w3a 1084   ∈ wcel 2111  Vcvv 3442   class class class wbr 5034  ⟶wf 6328  –1-1-onto→wf1o 6331   ≈ cen 8507 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5171  ax-nul 5178  ax-pow 5235  ax-pr 5299  ax-un 7454 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3444  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4805  df-br 5035  df-opab 5097  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-fun 6334  df-fn 6335  df-f 6336  df-f1 6337  df-fo 6338  df-f1o 6339  df-en 8511 This theorem is referenced by:  f1oeng  8529  enrefg  8542  en2d  8546  en3d  8547  ener  8557  f1imaen2g  8571  cnven  8586  xpcomen  8609  omxpen  8620  pw2eng  8624  unfilem3  8786  xpfi  8791  hsmexlem1  9855  iccen  12895  uzenom  13347  nnenom  13363  eqgen  18346  dfod2  18704  hmphen  22431  clwlkclwwlken  27841  clwwlken  27881  clwwlknonclwlknonen  28192  dlwwlknondlwlknonen  28195
 Copyright terms: Public domain W3C validator