Theorem bren 4516

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 4514	. 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 993  E.wex 1015  Vcvv 1856   class class class wbr 2691  -1-1-onto->wf1o 3261   ~~ cen 4503

This theorem is referenced by:  domen 4518  ener 4549  en0 4562  ensn1 4563  en1 4565  ac6sfi 4589  canth2 4627  mapen 4636  ssenen 4649  phplem4 4656  php3 4660  ssfi 4681  unfilem3 4694  unifi 4699  fiint 4701  fodomfi 4707  numth2 4929  ruc 7759  infxpidmlem10 7771  infxpidmlem12 7773  infmap2lem1 7789  eqindhome 11007  fbssint 11521  fcluscomplem 11623

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 997  ax-gen 998  ax-8 999  ax-10 1001  ax-11 1002  ax-12 1003  ax-13 1004  ax-14 1005  ax-17 1006  ax-4 1008  ax-5o 1010  ax-6o 1013  ax-9o 1158  ax-10o 1176  ax-16 1246  ax-11o 1254  ax-ext 1499  ax-sep 2776  ax-pow 2817  ax-pr 2854  ax-un 3088

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-ex 1016  df-sb 1208  df-eu 1420  df-mo 1421  df-clab 1505  df-cleq 1510  df-clel 1513  df-ne 1629  df-v 1857  df-dif 2100  df-un 2101  df-in 2102  df-ss 2104  df-nul 2332  df-pw 2458  df-sn 2469  df-pr 2470  df-op 2473  df-uni 2569  df-br 2692  df-opab 2740  df-xp 3264  df-rel 3265  df-cnv 3266  df-dm 3268  df-rn 3269  df-fn 3273  df-f 3274  df-f1 3275  df-fo 3276  df-f1o 3277  df-en 4507

Copyright terms: Public domain