Theorem bren 8743

Description: Equinumerosity relation. (Contributed by NM, 15-Jun-1998.) (Proof shortened 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 8741	. 2 ⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
2		f1ofn 6717	. . . . 5 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝑓 Fn 𝐴)
3		fndm 6536	. . . . . 6 ⊢ (𝑓 Fn 𝐴 → dom 𝑓 = 𝐴)
4		vex 3436	. . . . . . 7 ⊢ 𝑓 ∈ V
5	4	dmex 7758	. . . . . 6 ⊢ dom 𝑓 ∈ V
6	3, 5	eqeltrrdi 2848	. . . . 5 ⊢ (𝑓 Fn 𝐴 → 𝐴 ∈ V)
7	2, 6	syl 17	. . . 4 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝐴 ∈ V)
8		f1ofo 6723	. . . . . 6 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝑓:𝐴–onto→𝐵)
9		forn 6691	. . . . . 6 ⊢ (𝑓:𝐴–onto→𝐵 → ran 𝑓 = 𝐵)
10	8, 9	syl 17	. . . . 5 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → ran 𝑓 = 𝐵)
11	4	rnex 7759	. . . . 5 ⊢ ran 𝑓 ∈ V
12	10, 11	eqeltrrdi 2848	. . . 4 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝐵 ∈ V)
13	7, 12	jca 512	. . 3 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
14	13	exlimiv 1933	. 2 ⊢ (∃𝑓 𝑓:𝐴–1-1-onto→𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
15		breng 8742	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴 ≈ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵))
16	1, 14, 15	pm5.21nii 380	1 ⊢ (𝐴 ≈ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵)

Syntax hints:   ↔ wb 205   ∧ wa 396   = wceq 1539  ∃wex 1782   ∈ wcel 2106  Vcvv 3432   class class class wbr 5074  dom cdm 5589  ran crn 5590   Fn wfn 6428  –onto→wfo 6431  –1-1-onto→wf1o 6432   ≈ cen 8730

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352  ax-un 7588

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-xp 5595  df-rel 5596  df-cnv 5597  df-dm 5599  df-rn 5600  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-en 8734

This theorem is referenced by:  domen  8751  f1oen3g  8754  ener  8787  en0OLD  8804  en0ALT  8805  ensn1OLD  8808  en1OLD  8812  en2snOLD  8832  unen  8836  enfixsn  8868  canth2  8917  mapen  8928  ssenen  8938  rexdif1en  8944  dif1en  8945  ssfiALT  8957  ensymfib  8970  entrfil  8971  phplem2  8991  php3  8995  phplem4OLD  9003  php3OLD  9007  isinf  9036  domunfican  9087  fiint  9091  mapfien2  9168  unxpwdom2  9347  isinffi  9750  infxpenc2  9778  fseqen  9783  dfac8b  9787  infpwfien  9818  dfac12r  9902  infmap2  9974  cff1  10014  infpssr  10064  fin4en1  10065  enfin2i  10077  enfin1ai  10140  axcc3  10194  axcclem  10213  numth  10228  ttukey2g  10272  canthnum  10405  canthwe  10407  canthp1  10410  pwfseq  10420  tskuni  10539  gruen  10568  hasheqf1o  14063  hashfacen  14166  hashfacenOLD  14167  fz1f1o  15422  ruc  15952  cnso  15956  eulerth  16484  ablfaclem3  19690  lbslcic  21048  uvcendim  21054  indishmph  22949  ufldom  23113  ovolctb  24654  ovoliunlem3  24668  iunmbl2  24721  dyadmbl  24764  vitali  24777  cusgrfilem3  27824  padct  31054  f1ocnt  31123  volmeas  32199  eulerpart  32349  derangenlem  33133  mblfinlem1  35814  sticksstones4  40105  sticksstones20  40122  eldioph2lem1  40582  isnumbasgrplem1  40926  nnf1oxpnn  42734  sprsymrelen  44952  prproropen  44960  uspgrspren  45314  uspgrbisymrel  45316  1aryenef  45991  2aryenef  46002  rrx2xpreen  46065