Theorem bren 8903

Description: Equinumerosity relation. (Contributed by NM, 15-Jun-1998.) Extract breng 8902 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 8901	. 2 ⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
2		f1ofn 6781	. . . . 5 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝑓 Fn 𝐴)
3		fndm 6601	. . . . . 6 ⊢ (𝑓 Fn 𝐴 → dom 𝑓 = 𝐴)
4		vex 3433	. . . . . . 7 ⊢ 𝑓 ∈ V
5	4	dmex 7860	. . . . . 6 ⊢ dom 𝑓 ∈ V
6	3, 5	eqeltrrdi 2845	. . . . 5 ⊢ (𝑓 Fn 𝐴 → 𝐴 ∈ V)
7	2, 6	syl 17	. . . 4 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝐴 ∈ V)
8		f1ofo 6787	. . . . . 6 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝑓:𝐴–onto→𝐵)
9		forn 6755	. . . . . 6 ⊢ (𝑓:𝐴–onto→𝐵 → ran 𝑓 = 𝐵)
10	8, 9	syl 17	. . . . 5 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → ran 𝑓 = 𝐵)
11	4	rnex 7861	. . . . 5 ⊢ ran 𝑓 ∈ V
12	10, 11	eqeltrrdi 2845	. . . 4 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝐵 ∈ V)
13	7, 12	jca 511	. . 3 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
14	13	exlimiv 1932	. 2 ⊢ (∃𝑓 𝑓:𝐴–1-1-onto→𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
15		breng 8902	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴 ≈ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵))
16	1, 14, 15	pm5.21nii 378	1 ⊢ (𝐴 ≈ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵)

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1542  ∃wex 1781   ∈ wcel 2114  Vcvv 3429   class class class wbr 5085  dom cdm 5631  ran crn 5632   Fn wfn 6493  –onto→wfo 6496  –1-1-onto→wf1o 6497   ≈ cen 8890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-sep 5231  ax-pr 5375  ax-un 7689

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-xp 5637  df-rel 5638  df-cnv 5639  df-dm 5641  df-rn 5642  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-en 8894

This theorem is referenced by:  domen  8908  f1oen3g  8913  ener  8948  en0ALT  8966  unen  8992  enfixsn  9024  canth2  9068  mapen  9079  ssenen  9089  dif1en  9096  ssfiALT  9108  ensymfib  9118  entrfil  9119  phplem2  9139  php3  9143  isinf  9175  domunfican  9232  fiint  9237  mapfien2  9322  unxpwdom2  9503  isinffi  9916  infxpenc2  9944  fseqen  9949  dfac8b  9953  infpwfien  9984  dfac12r  10069  infmap2  10139  cff1  10180  infpssr  10230  fin4en1  10231  enfin2i  10243  enfin1ai  10306  axcc3  10360  axcclem  10379  numth  10394  ttukey2g  10438  canthnum  10572  canthwe  10574  canthp1  10577  pwfseq  10587  tskuni  10706  gruen  10735  hasheqf1o  14311  hashfacen  14416  fz1f1o  15672  ruc  16210  cnso  16214  eulerth  16753  ablfaclem3  20064  lbslcic  21821  uvcendim  21827  indishmph  23763  ufldom  23927  ovolctb  25457  ovoliunlem3  25471  iunmbl2  25524  dyadmbl  25567  vitali  25580  cusgrfilem3  29526  padct  32791  f1ocnt  32873  volmeas  34375  eulerpart  34526  derangenlem  35353  mblfinlem1  37978  sticksstones4  42588  sticksstones20  42605  eldioph2lem1  43192  isnumbasgrplem1  43529  nnf1oxpnn  45625  sprsymrelen  47960  prproropen  47968  uspgrspren  48628  uspgrbisymrel  48630  1aryenef  49121  2aryenef  49132  rrx2xpreen  49195