Theorem bren 8928

Description: Equinumerosity relation. (Contributed by NM, 15-Jun-1998.) Extract breng 8927 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 8926	. 2 ⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
2		f1ofn 6801	. . . . 5 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝑓 Fn 𝐴)
3		fndm 6621	. . . . . 6 ⊢ (𝑓 Fn 𝐴 → dom 𝑓 = 𝐴)
4		vex 3451	. . . . . . 7 ⊢ 𝑓 ∈ V
5	4	dmex 7885	. . . . . 6 ⊢ dom 𝑓 ∈ V
6	3, 5	eqeltrrdi 2837	. . . . 5 ⊢ (𝑓 Fn 𝐴 → 𝐴 ∈ V)
7	2, 6	syl 17	. . . 4 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝐴 ∈ V)
8		f1ofo 6807	. . . . . 6 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝑓:𝐴–onto→𝐵)
9		forn 6775	. . . . . 6 ⊢ (𝑓:𝐴–onto→𝐵 → ran 𝑓 = 𝐵)
10	8, 9	syl 17	. . . . 5 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → ran 𝑓 = 𝐵)
11	4	rnex 7886	. . . . 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 8927	. 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 3447   class class class wbr 5107  dom cdm 5638  ran crn 5639   Fn wfn 6506  –onto→wfo 6509  –1-1-onto→wf1o 6510   ≈ cen 8915

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 5251  ax-nul 5261  ax-pr 5387  ax-un 7711

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 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-xp 5644  df-rel 5645  df-cnv 5646  df-dm 5648  df-rn 5649  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-en 8919

This theorem is referenced by:  domen  8933  f1oen3g  8938  ener  8972  en0ALT  8990  unen  9017  enfixsn  9050  canth2  9094  mapen  9105  ssenen  9115  rexdif1enOLD  9123  dif1en  9124  dif1enOLD  9126  ssfiALT  9138  ensymfib  9148  entrfil  9149  phplem2  9169  php3  9173  isinf  9207  isinfOLD  9208  domunfican  9272  fiint  9277  fiintOLD  9278  mapfien2  9360  unxpwdom2  9541  isinffi  9945  infxpenc2  9975  fseqen  9980  dfac8b  9984  infpwfien  10015  dfac12r  10100  infmap2  10170  cff1  10211  infpssr  10261  fin4en1  10262  enfin2i  10274  enfin1ai  10337  axcc3  10391  axcclem  10410  numth  10425  ttukey2g  10469  canthnum  10602  canthwe  10604  canthp1  10607  pwfseq  10617  tskuni  10736  gruen  10765  hasheqf1o  14314  hashfacen  14419  fz1f1o  15676  ruc  16211  cnso  16215  eulerth  16753  ablfaclem3  20019  lbslcic  21750  uvcendim  21756  indishmph  23685  ufldom  23849  ovolctb  25391  ovoliunlem3  25405  iunmbl2  25458  dyadmbl  25501  vitali  25514  cusgrfilem3  29385  padct  32643  f1ocnt  32725  volmeas  34221  eulerpart  34373  derangenlem  35158  mblfinlem1  37651  sticksstones4  42137  sticksstones20  42154  eldioph2lem1  42748  isnumbasgrplem1  43090  nnf1oxpnn  45189  sprsymrelen  47501  prproropen  47509  uspgrspren  48140  uspgrbisymrel  48142  1aryenef  48634  2aryenef  48645  rrx2xpreen  48708