Theorem bren 8885

Description: Equinumerosity relation. (Contributed by NM, 15-Jun-1998.) Extract breng 8884 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 8883	. 2 ⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
2		f1ofn 6769	. . . . 5 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝑓 Fn 𝐴)
3		fndm 6589	. . . . . 6 ⊢ (𝑓 Fn 𝐴 → dom 𝑓 = 𝐴)
4		vex 3441	. . . . . . 7 ⊢ 𝑓 ∈ V
5	4	dmex 7845	. . . . . 6 ⊢ dom 𝑓 ∈ V
6	3, 5	eqeltrrdi 2842	. . . . 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 7846	. . . . 5 ⊢ ran 𝑓 ∈ V
12	10, 11	eqeltrrdi 2842	. . . 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 8884	. 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 3437   class class class wbr 5093  dom cdm 5619  ran crn 5620   Fn wfn 6481  –onto→wfo 6484  –1-1-onto→wf1o 6485   ≈ cen 8872

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 2705  ax-sep 5236  ax-nul 5246  ax-pr 5372  ax-un 7674

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 2712  df-cleq 2725  df-clel 2808  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-opab 5156  df-xp 5625  df-rel 5626  df-cnv 5627  df-dm 5629  df-rn 5630  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-en 8876

This theorem is referenced by:  domen  8890  f1oen3g  8895  ener  8930  en0ALT  8948  unen  8974  enfixsn  9006  canth2  9050  mapen  9061  ssenen  9071  dif1en  9078  ssfiALT  9090  ensymfib  9100  entrfil  9101  phplem2  9121  php3  9125  isinf  9156  domunfican  9213  fiint  9218  mapfien2  9300  unxpwdom2  9481  isinffi  9892  infxpenc2  9920  fseqen  9925  dfac8b  9929  infpwfien  9960  dfac12r  10045  infmap2  10115  cff1  10156  infpssr  10206  fin4en1  10207  enfin2i  10219  enfin1ai  10282  axcc3  10336  axcclem  10355  numth  10370  ttukey2g  10414  canthnum  10547  canthwe  10549  canthp1  10552  pwfseq  10562  tskuni  10681  gruen  10710  hasheqf1o  14258  hashfacen  14363  fz1f1o  15619  ruc  16154  cnso  16158  eulerth  16696  ablfaclem3  20003  lbslcic  21780  uvcendim  21786  indishmph  23714  ufldom  23878  ovolctb  25419  ovoliunlem3  25433  iunmbl2  25486  dyadmbl  25529  vitali  25542  cusgrfilem3  29438  padct  32705  f1ocnt  32787  volmeas  34265  eulerpart  34416  derangenlem  35236  mblfinlem1  37717  sticksstones4  42262  sticksstones20  42279  eldioph2lem1  42877  isnumbasgrplem1  43218  nnf1oxpnn  45316  sprsymrelen  47624  prproropen  47632  uspgrspren  48276  uspgrbisymrel  48278  1aryenef  48770  2aryenef  48781  rrx2xpreen  48844