Theorem bren 8900

Description: Equinumerosity relation. (Contributed by NM, 15-Jun-1998.) Extract breng 8899 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 8898	. 2 ⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
2		f1ofn 6775	. . . . 5 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝑓 Fn 𝐴)
3		fndm 6595	. . . . . 6 ⊢ (𝑓 Fn 𝐴 → dom 𝑓 = 𝐴)
4		vex 3436	. . . . . . 7 ⊢ 𝑓 ∈ V
5	4	dmex 7856	. . . . . 6 ⊢ dom 𝑓 ∈ V
6	3, 5	eqeltrrdi 2849	. . . . 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 7857	. . . . 5 ⊢ ran 𝑓 ∈ V
12	10, 11	eqeltrrdi 2849	. . . 4 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝐵 ∈ V)
13	7, 12	jca 516	. . 3 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
14	13	exlimiv 1937	. 2 ⊢ (∃𝑓 𝑓:𝐴–1-1-onto→𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
15		breng 8899	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴 ≈ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵))
16	1, 14, 15	pm5.21nii 379	1 ⊢ (𝐴 ≈ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵)

Syntax hints:   ↔ wb 207   ∧ wa 396   = wceq 1547  ∃wex 1786   ∈ wcel 2119  Vcvv 3432   class class class wbr 5079  dom cdm 5625  ran crn 5626   Fn wfn 6487  –onto→wfo 6490  –1-1-onto→wf1o 6491   ≈ cen 8887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-sep 5225  ax-pr 5369  ax-un 7685

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-xp 5631  df-rel 5632  df-cnv 5633  df-dm 5635  df-rn 5636  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-en 8891

This theorem is referenced by:  domen  8905  f1oen3g  8910  ener  8945  en0ALT  8963  unen  8989  enfixsn  9021  canth2  9065  mapen  9076  ssenen  9086  dif1en  9093  ssfiALT  9105  ensymfib  9115  entrfil  9116  phplem2  9136  php3  9140  isinf  9172  domunfican  9229  fiint  9234  mapfien2  9319  unxpwdom2  9500  isinffi  9914  infxpenc2  9942  fseqen  9947  dfac8b  9951  infpwfien  9982  dfac12r  10067  infmap2  10137  cff1  10178  infpssr  10228  fin4en1  10229  enfin2i  10241  enfin1ai  10304  axcc3  10358  axcclem  10377  numth  10392  ttukey2g  10436  canthnum  10570  canthwe  10572  canthp1  10575  pwfseq  10585  tskuni  10704  gruen  10733  hasheqf1o  14309  hashfacen  14414  fz1f1o  15670  ruc  16208  cnso  16212  eulerth  16751  ablfaclem3  20062  lbslcic  21823  uvcendim  21829  indishmph  23788  ufldom  23952  ovolctb  25482  ovoliunlem3  25496  iunmbl2  25549  dyadmbl  25592  vitali  25605  cusgrfilem3  29551  padct  32817  f1ocnt  32899  volmeas  34422  eulerpart  34573  derangenlem  35406  mblfinlem1  38031  sticksstones4  42641  sticksstones20  42658  eldioph2lem1  43216  isnumbasgrplem1  43553  nnf1oxpnn  45649  sprsymrelen  47982  prproropen  47990  uspgrspren  48650  uspgrbisymrel  48652  1aryenef  49143  2aryenef  49154  rrx2xpreen  49217