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

Theorem f1oen2g 7074
 Description: The domain and range of a one-to-one, onto function are equinumerous. This variation of f1oeng 7076 does not require the Axiom of Replacement. (Contributed by Mario Carneiro, 10-Sep-2015.)
Assertion
Ref Expression
f1oen2g

Proof of Theorem f1oen2g
StepHypRef Expression
1 f1of 5628 . . . 4
2 fex2 5557 . . . 4
31, 2syl3an1 1217 . . 3
433coml 1160 . 2
5 simp3 959 . 2
6 f1oen3g 7073 . 2
74, 5, 6syl2anc 643 1
 Colors of variables: wff set class Syntax hints:   wi 4   w3a 936   wcel 1721  cvv 2913   class class class wbr 4167  wf 5404  wf1o 5407   cen 7056 This theorem is referenced by:  f1oeng  7076  enrefg  7089  en2d  7093  en3d  7094  ener  7104  f1imaen2g  7118  cnven  7132  xpcomen  7149  omxpen  7160  pw2eng  7164  unfilem3  7323  xpfi  7328  hsmexlem1  8253  iccen  10986  uzenom  11245  nnenom  11260  hashf1rn  11577  eqgen  14934  dfod2  15141  hmphen  17756  0sgmppw  20921 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2382  ax-sep 4285  ax-nul 4293  ax-pow 4332  ax-pr 4358  ax-un 4655 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2256  df-mo 2257  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2526  df-ne 2566  df-ral 2668  df-rex 2669  df-rab 2672  df-v 2915  df-dif 3280  df-un 3282  df-in 3284  df-ss 3291  df-nul 3586  df-if 3697  df-pw 3758  df-sn 3777  df-pr 3778  df-op 3780  df-uni 3972  df-br 4168  df-opab 4222  df-xp 4838  df-rel 4839  df-cnv 4840  df-co 4841  df-dm 4842  df-rn 4843  df-fun 5410  df-fn 5411  df-f 5412  df-f1 5413  df-fo 5414  df-f1o 5415  df-en 7060
 Copyright terms: Public domain W3C validator