Theorem bren 8931

Description: Equinumerosity relation. (Contributed by NM, 15-Jun-1998.) Extract breng 8930 as an intermediate result. (Revised by BTernaryTau, 23-Sep-2024.)

Assertion

Ref	Expression
bren	⊢ (𝐴 ≈ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵)

Distinct variable groups:   𝐴,𝑓   𝐵,𝑓

Proof of Theorem bren

Step	Hyp	Ref	Expression
1		encv 8929	. 2 ⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
2		f1ofn 6804	. . . . 5 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝑓 Fn 𝐴)
3		fndm 6624	. . . . . 6 ⊢ (𝑓 Fn 𝐴 → dom 𝑓 = 𝐴)
4		vex 3454	. . . . . . 7 ⊢ 𝑓 ∈ V
5	4	dmex 7888	. . . . . 6 ⊢ dom 𝑓 ∈ V
6	3, 5	eqeltrrdi 2838	. . . . 5 ⊢ (𝑓 Fn 𝐴 → 𝐴 ∈ V)
7	2, 6	syl 17	. . . 4 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝐴 ∈ V)
8		f1ofo 6810	. . . . . 6 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝑓:𝐴–onto→𝐵)
9		forn 6778	. . . . . 6 ⊢ (𝑓:𝐴–onto→𝐵 → ran 𝑓 = 𝐵)
10	8, 9	syl 17	. . . . 5 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → ran 𝑓 = 𝐵)
11	4	rnex 7889	. . . . 5 ⊢ ran 𝑓 ∈ V
12	10, 11	eqeltrrdi 2838	. . . 4 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝐵 ∈ V)
13	7, 12	jca 511	. . 3 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
14	13	exlimiv 1930	. 2 ⊢ (∃𝑓 𝑓:𝐴–1-1-onto→𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
15		breng 8930	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴 ≈ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵))
16	1, 14, 15	pm5.21nii 378	1 ⊢ (𝐴 ≈ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵)

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1540  ∃wex 1779   ∈ wcel 2109  Vcvv 3450   class class class wbr 5110  dom cdm 5641  ran crn 5642   Fn wfn 6509  –onto→wfo 6512  –1-1-onto→wf1o 6513   ≈ cen 8918

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390  ax-un 7714

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-xp 5647  df-rel 5648  df-cnv 5649  df-dm 5651  df-rn 5652  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-en 8922

This theorem is referenced by:  domen  8936  f1oen3g  8941  ener  8975  en0ALT  8993  unen  9020  enfixsn  9055  canth2  9100  mapen  9111  ssenen  9121  rexdif1enOLD  9129  dif1en  9130  dif1enOLD  9132  ssfiALT  9144  ensymfib  9154  entrfil  9155  phplem2  9175  php3  9179  isinf  9214  isinfOLD  9215  domunfican  9279  fiint  9284  fiintOLD  9285  mapfien2  9367  unxpwdom2  9548  isinffi  9952  infxpenc2  9982  fseqen  9987  dfac8b  9991  infpwfien  10022  dfac12r  10107  infmap2  10177  cff1  10218  infpssr  10268  fin4en1  10269  enfin2i  10281  enfin1ai  10344  axcc3  10398  axcclem  10417  numth  10432  ttukey2g  10476  canthnum  10609  canthwe  10611  canthp1  10614  pwfseq  10624  tskuni  10743  gruen  10772  hasheqf1o  14321  hashfacen  14426  fz1f1o  15683  ruc  16218  cnso  16222  eulerth  16760  ablfaclem3  20026  lbslcic  21757  uvcendim  21763  indishmph  23692  ufldom  23856  ovolctb  25398  ovoliunlem3  25412  iunmbl2  25465  dyadmbl  25508  vitali  25521  cusgrfilem3  29392  padct  32650  f1ocnt  32732  volmeas  34228  eulerpart  34380  derangenlem  35165  mblfinlem1  37658  sticksstones4  42144  sticksstones20  42161  eldioph2lem1  42755  isnumbasgrplem1  43097  nnf1oxpnn  45196  sprsymrelen  47505  prproropen  47513  uspgrspren  48144  uspgrbisymrel  48146  1aryenef  48638  2aryenef  48649  rrx2xpreen  48712