Theorem bren 8986

Description: Equinumerosity relation. (Contributed by NM, 15-Jun-1998.) Extract breng 8985 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 8984	. 2 ⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
2		f1ofn 6825	. . . . 5 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝑓 Fn 𝐴)
3		fndm 6642	. . . . . 6 ⊢ (𝑓 Fn 𝐴 → dom 𝑓 = 𝐴)
4		vex 3454	. . . . . . 7 ⊢ 𝑓 ∈ V
5	4	dmex 7921	. . . . . 6 ⊢ dom 𝑓 ∈ V
6	3, 5	eqeltrrdi 2869	. . . . 5 ⊢ (𝑓 Fn 𝐴 → 𝐴 ∈ V)
7	2, 6	syl 18	. . . 4 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝐴 ∈ V)
8		f1ofo 6832	. . . . . 6 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝑓:𝐴–onto→𝐵)
9		forn 6799	. . . . . 6 ⊢ (𝑓:𝐴–onto→𝐵 → ran 𝑓 = 𝐵)
10	8, 9	syl 18	. . . . 5 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → ran 𝑓 = 𝐵)
11	4	rnex 7922	. . . . 5 ⊢ ran 𝑓 ∈ V
12	10, 11	eqeltrrdi 2869	. . . 4 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝐵 ∈ V)
13	7, 12	jca 521	. . 3 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
14	13	exlimiv 1962	. 2 ⊢ (∃𝑓 𝑓:𝐴–1-1-onto→𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
15		breng 8985	. 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 1569  ∃wex 1811   ∈ wcel 2144  Vcvv 3450   class class class wbr 5102  dom cdm 5650  ran crn 5651   Fn wfn 6533  –onto→wfo 6536  –1-1-onto→wf1o 6537   ≈ cen 8973

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5390  ax-un 7751

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-xp 5656  df-rel 5657  df-cnv 5658  df-dm 5660  df-rn 5661  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-en 8977

This theorem is used by:  domen  8991  f1oen3g  8996  ener  9031  en0ALT  9049  unen  9076  enfixsn  9108  canth2  9152  mapen  9163  ssenen  9173  dif1en  9180  ssfiALT  9192  ensymfib  9202  entrfil  9203  phplem2  9223  php3  9227  isinf  9259  domunfican  9316  fiint  9321  mapfien2  9404  unxpwdom2  9585  isinffi  10076  infxpenc2  10104  fseqen  10109  dfac8b  10113  infpwfien  10144  dfac12r  10228  infmap2  10298  cff1  10339  infpssr  10389  fin4en1  10390  enfin2i  10402  enfin1ai  10465  axcc3  10519  axcclem  10538  numth  10553  ttukey2g  10597  canthnum  10737  canthwe  10739  canthp1  10742  pwfseq  10752  tskuni  10871  gruen  10900  hasheqf1o  14496  hashfacen  14602  fz1f1o  15881  ruc  16416  cnso  16420  eulerth  16965  ablfaclem3  20308  lbslcic  22152  uvcendim  22158  indishmph  24122  ufldom  24286  ovolctb  25816  ovoliunlem3  25830  iunmbl2  25883  dyadmbl  25926  vitali  25939  cusgrfilem3  30043  padct  33357  f1ocnt  33438  volmeas  34910  eulerpart  35060  dfac15  35809  derangenlem  36022  mblfinlem1  38668  sticksstones4  43292  sticksstones20  43309  eldioph2lem1  43864  isnumbasgrplem1  44196  nnf1oxpnn  46303  sprsymrelen  48675  prproropen  48683  uspgrspren  49343  uspgrbisymrel  49345  1aryenef  49850  2aryenef  49861  rrx2xpreen  49925