Theorem bren 8977

Description: Equinumerosity relation. (Contributed by NM, 15-Jun-1998.) Extract breng 8976 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 8975	. 2 ⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
2		f1ofn 6829	. . . . 5 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝑓 Fn 𝐴)
3		fndm 6651	. . . . . 6 ⊢ (𝑓 Fn 𝐴 → dom 𝑓 = 𝐴)
4		vex 3467	. . . . . . 7 ⊢ 𝑓 ∈ V
5	4	dmex 7913	. . . . . 6 ⊢ dom 𝑓 ∈ V
6	3, 5	eqeltrrdi 2842	. . . . 5 ⊢ (𝑓 Fn 𝐴 → 𝐴 ∈ V)
7	2, 6	syl 17	. . . 4 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝐴 ∈ V)
8		f1ofo 6835	. . . . . 6 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝑓:𝐴–onto→𝐵)
9		forn 6803	. . . . . 6 ⊢ (𝑓:𝐴–onto→𝐵 → ran 𝑓 = 𝐵)
10	8, 9	syl 17	. . . . 5 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → ran 𝑓 = 𝐵)
11	4	rnex 7914	. . . . 5 ⊢ ran 𝑓 ∈ V
12	10, 11	eqeltrrdi 2842	. . . 4 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝐵 ∈ V)
13	7, 12	jca 511	. . 3 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
14	13	exlimiv 1929	. 2 ⊢ (∃𝑓 𝑓:𝐴–1-1-onto→𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
15		breng 8976	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴 ≈ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵))
16	1, 14, 15	pm5.21nii 378	1 ⊢ (𝐴 ≈ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵)

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1539  ∃wex 1778   ∈ wcel 2107  Vcvv 3463   class class class wbr 5123  dom cdm 5665  ran crn 5666   Fn wfn 6536  –onto→wfo 6539  –1-1-onto→wf1o 6540   ≈ cen 8964

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706  ax-sep 5276  ax-nul 5286  ax-pr 5412  ax-un 7737

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-ral 3051  df-rex 3060  df-rab 3420  df-v 3465  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4888  df-br 5124  df-opab 5186  df-xp 5671  df-rel 5672  df-cnv 5673  df-dm 5675  df-rn 5676  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-en 8968

This theorem is referenced by:  domen  8984  f1oen3g  8989  ener  9023  en0ALT  9041  unen  9068  enfixsn  9103  canth2  9152  mapen  9163  ssenen  9173  rexdif1enOLD  9181  dif1en  9182  dif1enOLD  9184  ssfiALT  9196  ensymfib  9206  entrfil  9207  phplem2  9227  php3  9231  phplem4OLD  9239  php3OLD  9243  isinf  9278  isinfOLD  9279  domunfican  9343  fiint  9348  fiintOLD  9349  mapfien2  9431  unxpwdom2  9610  isinffi  10014  infxpenc2  10044  fseqen  10049  dfac8b  10053  infpwfien  10084  dfac12r  10169  infmap2  10239  cff1  10280  infpssr  10330  fin4en1  10331  enfin2i  10343  enfin1ai  10406  axcc3  10460  axcclem  10479  numth  10494  ttukey2g  10538  canthnum  10671  canthwe  10673  canthp1  10676  pwfseq  10686  tskuni  10805  gruen  10834  hasheqf1o  14371  hashfacen  14476  fz1f1o  15729  ruc  16262  cnso  16266  eulerth  16803  ablfaclem3  20076  lbslcic  21816  uvcendim  21822  indishmph  23753  ufldom  23917  ovolctb  25462  ovoliunlem3  25476  iunmbl2  25529  dyadmbl  25572  vitali  25585  cusgrfilem3  29404  padct  32667  f1ocnt  32748  volmeas  34207  eulerpart  34359  derangenlem  35151  mblfinlem1  37639  sticksstones4  42125  sticksstones20  42142  eldioph2lem1  42749  isnumbasgrplem1  43091  nnf1oxpnn  45172  sprsymrelen  47460  prproropen  47468  uspgrspren  48041  uspgrbisymrel  48043  1aryenef  48539  2aryenef  48550  rrx2xpreen  48613