Theorem bren 8896

Description: Equinumerosity relation. (Contributed by NM, 15-Jun-1998.) Extract breng 8895 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 8894	. 2 ⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
2		f1ofn 6775	. . . . 5 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝑓 Fn 𝐴)
3		fndm 6595	. . . . . 6 ⊢ (𝑓 Fn 𝐴 → dom 𝑓 = 𝐴)
4		vex 3434	. . . . . . 7 ⊢ 𝑓 ∈ V
5	4	dmex 7853	. . . . . 6 ⊢ dom 𝑓 ∈ V
6	3, 5	eqeltrrdi 2846	. . . . 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 7854	. . . . 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 8895	. 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 3430   class class class wbr 5086  dom cdm 5624  ran crn 5625   Fn wfn 6487  –onto→wfo 6490  –1-1-onto→wf1o 6491   ≈ cen 8883

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 5231  ax-pr 5370  ax-un 7682

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 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  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 8887

This theorem is referenced by:  domen  8901  f1oen3g  8906  ener  8941  en0ALT  8959  unen  8985  enfixsn  9017  canth2  9061  mapen  9072  ssenen  9082  dif1en  9089  ssfiALT  9101  ensymfib  9111  entrfil  9112  phplem2  9132  php3  9136  isinf  9168  domunfican  9225  fiint  9230  mapfien2  9315  unxpwdom2  9496  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  10563  canthwe  10565  canthp1  10568  pwfseq  10578  tskuni  10697  gruen  10726  hasheqf1o  14302  hashfacen  14407  fz1f1o  15663  ruc  16201  cnso  16205  eulerth  16744  ablfaclem3  20055  lbslcic  21831  uvcendim  21837  indishmph  23773  ufldom  23937  ovolctb  25467  ovoliunlem3  25481  iunmbl2  25534  dyadmbl  25577  vitali  25590  cusgrfilem3  29541  padct  32806  f1ocnt  32888  volmeas  34391  eulerpart  34542  derangenlem  35369  mblfinlem1  37992  sticksstones4  42602  sticksstones20  42619  eldioph2lem1  43206  isnumbasgrplem1  43547  nnf1oxpnn  45643  sprsymrelen  47972  prproropen  47980  uspgrspren  48640  uspgrbisymrel  48642  1aryenef  49133  2aryenef  49144  rrx2xpreen  49207