Theorem bren 8995

Description: Equinumerosity relation. (Contributed by NM, 15-Jun-1998.) Extract breng 8994 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 8993	. 2 ⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
2		f1ofn 6849	. . . . 5 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝑓 Fn 𝐴)
3		fndm 6671	. . . . . 6 ⊢ (𝑓 Fn 𝐴 → dom 𝑓 = 𝐴)
4		vex 3484	. . . . . . 7 ⊢ 𝑓 ∈ V
5	4	dmex 7931	. . . . . 6 ⊢ dom 𝑓 ∈ V
6	3, 5	eqeltrrdi 2850	. . . . 5 ⊢ (𝑓 Fn 𝐴 → 𝐴 ∈ V)
7	2, 6	syl 17	. . . 4 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝐴 ∈ V)
8		f1ofo 6855	. . . . . 6 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝑓:𝐴–onto→𝐵)
9		forn 6823	. . . . . 6 ⊢ (𝑓:𝐴–onto→𝐵 → ran 𝑓 = 𝐵)
10	8, 9	syl 17	. . . . 5 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → ran 𝑓 = 𝐵)
11	4	rnex 7932	. . . . 5 ⊢ ran 𝑓 ∈ V
12	10, 11	eqeltrrdi 2850	. . . 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 8994	. 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 3480   class class class wbr 5143  dom cdm 5685  ran crn 5686   Fn wfn 6556  –onto→wfo 6559  –1-1-onto→wf1o 6560   ≈ cen 8982

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 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-xp 5691  df-rel 5692  df-cnv 5693  df-dm 5695  df-rn 5696  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-en 8986

This theorem is referenced by:  domen  9002  f1oen3g  9007  ener  9041  en0ALT  9059  unen  9086  enfixsn  9121  canth2  9170  mapen  9181  ssenen  9191  rexdif1enOLD  9199  dif1en  9200  dif1enOLD  9202  ssfiALT  9214  ensymfib  9224  entrfil  9225  phplem2  9245  php3  9249  phplem4OLD  9257  php3OLD  9261  isinf  9296  isinfOLD  9297  domunfican  9361  fiint  9366  fiintOLD  9367  mapfien2  9449  unxpwdom2  9628  isinffi  10032  infxpenc2  10062  fseqen  10067  dfac8b  10071  infpwfien  10102  dfac12r  10187  infmap2  10257  cff1  10298  infpssr  10348  fin4en1  10349  enfin2i  10361  enfin1ai  10424  axcc3  10478  axcclem  10497  numth  10512  ttukey2g  10556  canthnum  10689  canthwe  10691  canthp1  10694  pwfseq  10704  tskuni  10823  gruen  10852  hasheqf1o  14388  hashfacen  14493  fz1f1o  15746  ruc  16279  cnso  16283  eulerth  16820  ablfaclem3  20107  lbslcic  21861  uvcendim  21867  indishmph  23806  ufldom  23970  ovolctb  25525  ovoliunlem3  25539  iunmbl2  25592  dyadmbl  25635  vitali  25648  cusgrfilem3  29475  padct  32731  f1ocnt  32804  volmeas  34232  eulerpart  34384  derangenlem  35176  mblfinlem1  37664  sticksstones4  42150  sticksstones20  42167  eldioph2lem1  42771  isnumbasgrplem1  43113  nnf1oxpnn  45200  sprsymrelen  47487  prproropen  47495  uspgrspren  48068  uspgrbisymrel  48070  1aryenef  48566  2aryenef  48577  rrx2xpreen  48640