Theorem bren 8926

Description: Equinumerosity relation. (Contributed by NM, 15-Jun-1998.) Extract breng 8925 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 8924	. 2 ⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
2		f1ofn 6796	. . . . 5 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝑓 Fn 𝐴)
3		fndm 6613	. . . . . 6 ⊢ (𝑓 Fn 𝐴 → dom 𝑓 = 𝐴)
4		vex 3452	. . . . . . 7 ⊢ 𝑓 ∈ V
5	4	dmex 7879	. . . . . 6 ⊢ dom 𝑓 ∈ V
6	3, 5	eqeltrrdi 2865	. . . . 5 ⊢ (𝑓 Fn 𝐴 → 𝐴 ∈ V)
7	2, 6	syl 17	. . . 4 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝐴 ∈ V)
8		f1ofo 6803	. . . . . 6 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝑓:𝐴–onto→𝐵)
9		forn 6770	. . . . . 6 ⊢ (𝑓:𝐴–onto→𝐵 → ran 𝑓 = 𝐵)
10	8, 9	syl 17	. . . . 5 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → ran 𝑓 = 𝐵)
11	4	rnex 7880	. . . . 5 ⊢ ran 𝑓 ∈ V
12	10, 11	eqeltrrdi 2865	. . . 4 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝐵 ∈ V)
13	7, 12	jca 518	. . 3 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
14	13	exlimiv 1944	. 2 ⊢ (∃𝑓 𝑓:𝐴–1-1-onto→𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
15		breng 8925	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴 ≈ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵))
16	1, 14, 15	pm5.21nii 380	1 ⊢ (𝐴 ≈ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵)

Syntax hints:   ↔ wb 208   ∧ wa 398   = wceq 1554  ∃wex 1793   ∈ wcel 2136  Vcvv 3448   class class class wbr 5094  dom cdm 5640  ran crn 5641   Fn wfn 6505  –onto→wfo 6508  –1-1-onto→wf1o 6509   ≈ cen 8913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-ext 2728  ax-sep 5240  ax-pr 5384  ax-un 7707

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1557  df-fal 1567  df-ex 1794  df-sb 2085  df-clab 2735  df-cleq 2748  df-clel 2831  df-ral 3071  df-rex 3081  df-rab 3409  df-v 3450  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4281  df-if 4475  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5095  df-opab 5157  df-xp 5646  df-rel 5647  df-cnv 5648  df-dm 5650  df-rn 5651  df-fn 6513  df-f 6514  df-f1 6515  df-fo 6516  df-f1o 6517  df-en 8917

This theorem is referenced by:  domen  8931  f1oen3g  8936  ener  8971  en0ALT  8989  unen  9015  enfixsn  9047  canth2  9091  mapen  9102  ssenen  9112  dif1en  9119  ssfiALT  9131  ensymfib  9141  entrfil  9142  phplem2  9162  php3  9166  isinf  9198  domunfican  9255  fiint  9260  mapfien2  9345  unxpwdom2  9526  isinffi  9940  infxpenc2  9968  fseqen  9973  dfac8b  9977  infpwfien  10008  dfac12r  10093  infmap2  10163  cff1  10205  infpssr  10255  fin4en1  10256  enfin2i  10268  enfin1ai  10331  axcc3  10385  axcclem  10404  numth  10419  ttukey2g  10463  canthnum  10597  canthwe  10599  canthp1  10602  pwfseq  10612  tskuni  10731  gruen  10760  hasheqf1o  14352  hashfacen  14457  fz1f1o  15713  ruc  16251  cnso  16255  eulerth  16794  ablfaclem3  20105  lbslcic  21866  uvcendim  21872  indishmph  23831  ufldom  23995  ovolctb  25525  ovoliunlem3  25539  iunmbl2  25592  dyadmbl  25635  vitali  25648  cusgrfilem3  29597  padct  32863  f1ocnt  32945  volmeas  34482  eulerpart  34633  derangenlem  35469  mblfinlem1  38104  sticksstones4  42714  sticksstones20  42731  eldioph2lem1  43289  isnumbasgrplem1  43626  nnf1oxpnn  45721  sprsymrelen  48054  prproropen  48062  uspgrspren  48722  uspgrbisymrel  48724  1aryenef  49215  2aryenef  49226  rrx2xpreen  49289