Theorem bren 8969

Description: Equinumerosity relation. (Contributed by NM, 15-Jun-1998.) Extract breng 8968 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 8967	. 2 ⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
2		f1ofn 6819	. . . . 5 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝑓 Fn 𝐴)
3		fndm 6641	. . . . . 6 ⊢ (𝑓 Fn 𝐴 → dom 𝑓 = 𝐴)
4		vex 3463	. . . . . . 7 ⊢ 𝑓 ∈ V
5	4	dmex 7905	. . . . . 6 ⊢ dom 𝑓 ∈ V
6	3, 5	eqeltrrdi 2843	. . . . 5 ⊢ (𝑓 Fn 𝐴 → 𝐴 ∈ V)
7	2, 6	syl 17	. . . 4 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝐴 ∈ V)
8		f1ofo 6825	. . . . . 6 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝑓:𝐴–onto→𝐵)
9		forn 6793	. . . . . 6 ⊢ (𝑓:𝐴–onto→𝐵 → ran 𝑓 = 𝐵)
10	8, 9	syl 17	. . . . 5 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → ran 𝑓 = 𝐵)
11	4	rnex 7906	. . . . 5 ⊢ ran 𝑓 ∈ V
12	10, 11	eqeltrrdi 2843	. . . 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 8968	. 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 2108  Vcvv 3459   class class class wbr 5119  dom cdm 5654  ran crn 5655   Fn wfn 6526  –onto→wfo 6529  –1-1-onto→wf1o 6530   ≈ cen 8956

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402  ax-un 7729

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-xp 5660  df-rel 5661  df-cnv 5662  df-dm 5664  df-rn 5665  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-en 8960

This theorem is referenced by:  domen  8976  f1oen3g  8981  ener  9015  en0ALT  9033  unen  9060  enfixsn  9095  canth2  9144  mapen  9155  ssenen  9165  rexdif1enOLD  9173  dif1en  9174  dif1enOLD  9176  ssfiALT  9188  ensymfib  9198  entrfil  9199  phplem2  9219  php3  9223  php3OLD  9233  isinf  9268  isinfOLD  9269  domunfican  9333  fiint  9338  fiintOLD  9339  mapfien2  9421  unxpwdom2  9602  isinffi  10006  infxpenc2  10036  fseqen  10041  dfac8b  10045  infpwfien  10076  dfac12r  10161  infmap2  10231  cff1  10272  infpssr  10322  fin4en1  10323  enfin2i  10335  enfin1ai  10398  axcc3  10452  axcclem  10471  numth  10486  ttukey2g  10530  canthnum  10663  canthwe  10665  canthp1  10668  pwfseq  10678  tskuni  10797  gruen  10826  hasheqf1o  14367  hashfacen  14472  fz1f1o  15726  ruc  16261  cnso  16265  eulerth  16802  ablfaclem3  20070  lbslcic  21801  uvcendim  21807  indishmph  23736  ufldom  23900  ovolctb  25443  ovoliunlem3  25457  iunmbl2  25510  dyadmbl  25553  vitali  25566  cusgrfilem3  29437  padct  32697  f1ocnt  32779  volmeas  34262  eulerpart  34414  derangenlem  35193  mblfinlem1  37681  sticksstones4  42162  sticksstones20  42179  eldioph2lem1  42783  isnumbasgrplem1  43125  nnf1oxpnn  45219  sprsymrelen  47514  prproropen  47522  uspgrspren  48127  uspgrbisymrel  48129  1aryenef  48625  2aryenef  48636  rrx2xpreen  48699