Theorem bren 4518

Description: Equinumerosity relation. Compare Definition of [Enderton] p. 129.

Hypothesis

Ref	Expression
bren.1	|- B e. V

Assertion

Ref	Expression
bren	|- (A ~~ B <-> E.f f:A-1-1-onto->B)

Distinct variable groups:   A,f   B,f

Proof of Theorem bren

Step	Hyp	Ref	Expression
1		bren.1	. 2 |- B e. V
2		breng 4516	. 2 |- (B e. V -> (A ~~ B <-> E.f f:A-1-1-onto->B))
3	1, 2	ax-mp 7	1 |- (A ~~ B <-> E.f f:A-1-1-onto->B)

Syntax hints:   <-> wb 144   e. wcel 994  E.wex 1016  Vcvv 1857   class class class wbr 2692  -1-1-onto->wf1o 3262   ~~ cen 4505

This theorem is referenced by:  domen 4520  ener 4551  en0 4564  ensn1 4565  en1 4567  ac6sfi 4591  canth2 4629  mapen 4638  ssenen 4651  phplem4 4658  php3 4662  ssfi 4683  unfilem3 4696  unifi 4701  fiint 4703  fodomfi 4709  numth2 4931  ruc 7761  infxpidmlem10 7773  infxpidmlem12 7775  infmap2lem1 7791  eqindhome 11047  finsschain 11425  fbssint 11626  fcluscomplem 11732

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-11 1003  ax-12 1004  ax-13 1005  ax-14 1006  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500  ax-sep 2777  ax-pow 2818  ax-pr 2855  ax-un 3089

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-ex 1017  df-sb 1209  df-eu 1421  df-mo 1422  df-clab 1506  df-cleq 1511  df-clel 1514  df-ne 1630  df-v 1858  df-dif 2101  df-un 2102  df-in 2103  df-ss 2105  df-nul 2333  df-pw 2459  df-sn 2470  df-pr 2471  df-op 2474  df-uni 2570  df-br 2693  df-opab 2741  df-xp 3265  df-rel 3266  df-cnv 3267  df-dm 3269  df-rn 3270  df-fn 3274  df-f 3275  df-f1 3276  df-fo 3277  df-f1o 3278  df-en 4509

Copyright terms: Public domain