Theorem bren 8893

Description: Equinumerosity relation. (Contributed by NM, 15-Jun-1998.) Extract breng 8892 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 8891	. 2 ⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
2		f1ofn 6775	. . . . 5 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝑓 Fn 𝐴)
3		fndm 6595	. . . . . 6 ⊢ (𝑓 Fn 𝐴 → dom 𝑓 = 𝐴)
4		vex 3444	. . . . . . 7 ⊢ 𝑓 ∈ V
5	4	dmex 7851	. . . . . 6 ⊢ dom 𝑓 ∈ V
6	3, 5	eqeltrrdi 2845	. . . . 5 ⊢ (𝑓 Fn 𝐴 → 𝐴 ∈ V)
7	2, 6	syl 17	. . . 4 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝐴 ∈ V)
8		f1ofo 6781	. . . . . 6 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝑓:𝐴–onto→𝐵)
9		forn 6749	. . . . . 6 ⊢ (𝑓:𝐴–onto→𝐵 → ran 𝑓 = 𝐵)
10	8, 9	syl 17	. . . . 5 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → ran 𝑓 = 𝐵)
11	4	rnex 7852	. . . . 5 ⊢ ran 𝑓 ∈ V
12	10, 11	eqeltrrdi 2845	. . . 4 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝐵 ∈ V)
13	7, 12	jca 511	. . 3 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
14	13	exlimiv 1931	. 2 ⊢ (∃𝑓 𝑓:𝐴–1-1-onto→𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
15		breng 8892	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴 ≈ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵))
16	1, 14, 15	pm5.21nii 378	1 ⊢ (𝐴 ≈ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵)

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1541  ∃wex 1780   ∈ wcel 2113  Vcvv 3440   class class class wbr 5098  dom cdm 5624  ran crn 5625   Fn wfn 6487  –onto→wfo 6490  –1-1-onto→wf1o 6491   ≈ cen 8880

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377  ax-un 7680

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-xp 5630  df-rel 5631  df-cnv 5632  df-dm 5634  df-rn 5635  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-en 8884

This theorem is referenced by:  domen  8898  f1oen3g  8903  ener  8938  en0ALT  8956  unen  8982  enfixsn  9014  canth2  9058  mapen  9069  ssenen  9079  dif1en  9086  ssfiALT  9098  ensymfib  9108  entrfil  9109  phplem2  9129  php3  9133  isinf  9165  domunfican  9222  fiint  9227  mapfien2  9312  unxpwdom2  9493  isinffi  9904  infxpenc2  9932  fseqen  9937  dfac8b  9941  infpwfien  9972  dfac12r  10057  infmap2  10127  cff1  10168  infpssr  10218  fin4en1  10219  enfin2i  10231  enfin1ai  10294  axcc3  10348  axcclem  10367  numth  10382  ttukey2g  10426  canthnum  10560  canthwe  10562  canthp1  10565  pwfseq  10575  tskuni  10694  gruen  10723  hasheqf1o  14272  hashfacen  14377  fz1f1o  15633  ruc  16168  cnso  16172  eulerth  16710  ablfaclem3  20018  lbslcic  21796  uvcendim  21802  indishmph  23742  ufldom  23906  ovolctb  25447  ovoliunlem3  25461  iunmbl2  25514  dyadmbl  25557  vitali  25570  cusgrfilem3  29531  padct  32797  f1ocnt  32880  volmeas  34388  eulerpart  34539  derangenlem  35365  mblfinlem1  37854  sticksstones4  42399  sticksstones20  42416  eldioph2lem1  42998  isnumbasgrplem1  43339  nnf1oxpnn  45435  sprsymrelen  47742  prproropen  47750  uspgrspren  48394  uspgrbisymrel  48396  1aryenef  48887  2aryenef  48898  rrx2xpreen  48961