Theorem bren 8889

Description: Equinumerosity relation. (Contributed by NM, 15-Jun-1998.) Extract breng 8888 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 8887	. 2 ⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
2		f1ofn 6769	. . . . 5 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝑓 Fn 𝐴)
3		fndm 6589	. . . . . 6 ⊢ (𝑓 Fn 𝐴 → dom 𝑓 = 𝐴)
4		vex 3442	. . . . . . 7 ⊢ 𝑓 ∈ V
5	4	dmex 7849	. . . . . 6 ⊢ dom 𝑓 ∈ V
6	3, 5	eqeltrrdi 2837	. . . . 5 ⊢ (𝑓 Fn 𝐴 → 𝐴 ∈ V)
7	2, 6	syl 17	. . . 4 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝐴 ∈ V)
8		f1ofo 6775	. . . . . 6 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝑓:𝐴–onto→𝐵)
9		forn 6743	. . . . . 6 ⊢ (𝑓:𝐴–onto→𝐵 → ran 𝑓 = 𝐵)
10	8, 9	syl 17	. . . . 5 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → ran 𝑓 = 𝐵)
11	4	rnex 7850	. . . . 5 ⊢ ran 𝑓 ∈ V
12	10, 11	eqeltrrdi 2837	. . . 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 8888	. 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 3438   class class class wbr 5095  dom cdm 5623  ran crn 5624   Fn wfn 6481  –onto→wfo 6484  –1-1-onto→wf1o 6485   ≈ cen 8876

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 2701  ax-sep 5238  ax-nul 5248  ax-pr 5374  ax-un 7675

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 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-xp 5629  df-rel 5630  df-cnv 5631  df-dm 5633  df-rn 5634  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-en 8880

This theorem is referenced by:  domen  8894  f1oen3g  8899  ener  8933  en0ALT  8951  unen  8978  enfixsn  9010  canth2  9054  mapen  9065  ssenen  9075  rexdif1enOLD  9083  dif1en  9084  dif1enOLD  9086  ssfiALT  9098  ensymfib  9108  entrfil  9109  phplem2  9129  php3  9133  isinf  9165  isinfOLD  9166  domunfican  9230  fiint  9235  fiintOLD  9236  mapfien2  9318  unxpwdom2  9499  isinffi  9907  infxpenc2  9935  fseqen  9940  dfac8b  9944  infpwfien  9975  dfac12r  10060  infmap2  10130  cff1  10171  infpssr  10221  fin4en1  10222  enfin2i  10234  enfin1ai  10297  axcc3  10351  axcclem  10370  numth  10385  ttukey2g  10429  canthnum  10562  canthwe  10564  canthp1  10567  pwfseq  10577  tskuni  10696  gruen  10725  hasheqf1o  14274  hashfacen  14379  fz1f1o  15635  ruc  16170  cnso  16174  eulerth  16712  ablfaclem3  19986  lbslcic  21766  uvcendim  21772  indishmph  23701  ufldom  23865  ovolctb  25407  ovoliunlem3  25421  iunmbl2  25474  dyadmbl  25517  vitali  25530  cusgrfilem3  29421  padct  32676  f1ocnt  32758  volmeas  34197  eulerpart  34349  derangenlem  35143  mblfinlem1  37636  sticksstones4  42122  sticksstones20  42139  eldioph2lem1  42733  isnumbasgrplem1  43074  nnf1oxpnn  45173  sprsymrelen  47485  prproropen  47493  uspgrspren  48137  uspgrbisymrel  48139  1aryenef  48631  2aryenef  48642  rrx2xpreen  48705