Theorem bren 8905

Description: Equinumerosity relation. (Contributed by NM, 15-Jun-1998.) Extract breng 8904 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 8903	. 2 ⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
2		f1ofn 6783	. . . . 5 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝑓 Fn 𝐴)
3		fndm 6603	. . . . . 6 ⊢ (𝑓 Fn 𝐴 → dom 𝑓 = 𝐴)
4		vex 3446	. . . . . . 7 ⊢ 𝑓 ∈ V
5	4	dmex 7861	. . . . . 6 ⊢ dom 𝑓 ∈ V
6	3, 5	eqeltrrdi 2846	. . . . 5 ⊢ (𝑓 Fn 𝐴 → 𝐴 ∈ V)
7	2, 6	syl 17	. . . 4 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝐴 ∈ V)
8		f1ofo 6789	. . . . . 6 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝑓:𝐴–onto→𝐵)
9		forn 6757	. . . . . 6 ⊢ (𝑓:𝐴–onto→𝐵 → ran 𝑓 = 𝐵)
10	8, 9	syl 17	. . . . 5 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → ran 𝑓 = 𝐵)
11	4	rnex 7862	. . . . 5 ⊢ ran 𝑓 ∈ V
12	10, 11	eqeltrrdi 2846	. . . 4 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝐵 ∈ V)
13	7, 12	jca 511	. . 3 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
14	13	exlimiv 1932	. 2 ⊢ (∃𝑓 𝑓:𝐴–1-1-onto→𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
15		breng 8904	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴 ≈ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵))
16	1, 14, 15	pm5.21nii 378	1 ⊢ (𝐴 ≈ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵)

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1542  ∃wex 1781   ∈ wcel 2114  Vcvv 3442   class class class wbr 5100  dom cdm 5632  ran crn 5633   Fn wfn 6495  –onto→wfo 6498  –1-1-onto→wf1o 6499   ≈ cen 8892

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243  ax-pr 5379  ax-un 7690

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-xp 5638  df-rel 5639  df-cnv 5640  df-dm 5642  df-rn 5643  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-en 8896

This theorem is referenced by:  domen  8910  f1oen3g  8915  ener  8950  en0ALT  8968  unen  8994  enfixsn  9026  canth2  9070  mapen  9081  ssenen  9091  dif1en  9098  ssfiALT  9110  ensymfib  9120  entrfil  9121  phplem2  9141  php3  9145  isinf  9177  domunfican  9234  fiint  9239  mapfien2  9324  unxpwdom2  9505  isinffi  9916  infxpenc2  9944  fseqen  9949  dfac8b  9953  infpwfien  9984  dfac12r  10069  infmap2  10139  cff1  10180  infpssr  10230  fin4en1  10231  enfin2i  10243  enfin1ai  10306  axcc3  10360  axcclem  10379  numth  10394  ttukey2g  10438  canthnum  10572  canthwe  10574  canthp1  10577  pwfseq  10587  tskuni  10706  gruen  10735  hasheqf1o  14284  hashfacen  14389  fz1f1o  15645  ruc  16180  cnso  16184  eulerth  16722  ablfaclem3  20030  lbslcic  21808  uvcendim  21814  indishmph  23754  ufldom  23918  ovolctb  25459  ovoliunlem3  25473  iunmbl2  25526  dyadmbl  25569  vitali  25582  cusgrfilem3  29543  padct  32807  f1ocnt  32890  volmeas  34408  eulerpart  34559  derangenlem  35384  mblfinlem1  37902  sticksstones4  42513  sticksstones20  42530  eldioph2lem1  43111  isnumbasgrplem1  43452  nnf1oxpnn  45548  sprsymrelen  47854  prproropen  47862  uspgrspren  48506  uspgrbisymrel  48508  1aryenef  48999  2aryenef  49010  rrx2xpreen  49073