Theorem bren 8962

Description: Equinumerosity relation. (Contributed by NM, 15-Jun-1998.) Extract breng 8961 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 8960	. 2 ⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
2		f1ofn 6828	. . . . 5 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝑓 Fn 𝐴)
3		fndm 6645	. . . . . 6 ⊢ (𝑓 Fn 𝐴 → dom 𝑓 = 𝐴)
4		vex 3462	. . . . . . 7 ⊢ 𝑓 ∈ V
5	4	dmex 7915	. . . . . 6 ⊢ dom 𝑓 ∈ V
6	3, 5	eqeltrrdi 2875	. . . . 5 ⊢ (𝑓 Fn 𝐴 → 𝐴 ∈ V)
7	2, 6	syl 18	. . . 4 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝐴 ∈ V)
8		f1ofo 6835	. . . . . 6 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝑓:𝐴–onto→𝐵)
9		forn 6802	. . . . . 6 ⊢ (𝑓:𝐴–onto→𝐵 → ran 𝑓 = 𝐵)
10	8, 9	syl 18	. . . . 5 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → ran 𝑓 = 𝐵)
11	4	rnex 7916	. . . . 5 ⊢ ran 𝑓 ∈ V
12	10, 11	eqeltrrdi 2875	. . . 4 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝐵 ∈ V)
13	7, 12	jca 521	. . 3 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
14	13	exlimiv 1963	. 2 ⊢ (∃𝑓 𝑓:𝐴–1-1-onto→𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
15		breng 8961	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴 ≈ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵))
16	1, 14, 15	pm5.21nii 381	1 ⊢ (𝐴 ≈ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵)

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   = wceq 1570  ∃wex 1812   ∈ wcel 2146  Vcvv 3458   class class class wbr 5114  dom cdm 5666  ran crn 5667   Fn wfn 6538  –onto→wfo 6541  –1-1-onto→wf1o 6542   ≈ cen 8949

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738  ax-sep 5262  ax-pr 5409  ax-un 7745

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-opab 5179  df-xp 5672  df-rel 5673  df-cnv 5674  df-dm 5676  df-rn 5677  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-en 8953

This theorem is used by:  domen  8967  f1oen3g  8972  ener  9007  en0ALT  9025  unen  9052  enfixsn  9084  canth2  9128  mapen  9139  ssenen  9149  dif1en  9156  ssfiALT  9168  ensymfib  9178  entrfil  9179  phplem2  9199  php3  9203  isinf  9235  domunfican  9291  fiint  9296  mapfien2  9379  unxpwdom2  9560  isinffi  9997  infxpenc2  10025  fseqen  10030  dfac8b  10034  infpwfien  10065  dfac12r  10149  infmap2  10219  cff1  10260  infpssr  10310  fin4en1  10311  enfin2i  10323  enfin1ai  10386  axcc3  10440  axcclem  10459  numth  10474  ttukey2g  10518  canthnum  10652  canthwe  10654  canthp1  10657  pwfseq  10667  tskuni  10786  gruen  10815  hasheqf1o  14405  hashfacen  14511  fz1f1o  15787  ruc  16324  cnso  16328  eulerth  16867  ablfaclem3  20190  lbslcic  22028  uvcendim  22034  indishmph  23992  ufldom  24156  ovolctb  25686  ovoliunlem3  25700  iunmbl2  25753  dyadmbl  25796  vitali  25809  cusgrfilem3  29844  padct  33100  f1ocnt  33182  volmeas  34653  eulerpart  34804  derangenlem  35684  mblfinlem1  38349  sticksstones4  42957  sticksstones20  42974  eldioph2lem1  43532  isnumbasgrplem1  43869  nnf1oxpnn  45954  sprsymrelen  48290  prproropen  48298  uspgrspren  48958  uspgrbisymrel  48960  1aryenef  49466  2aryenef  49477  rrx2xpreen  49540