Theorem bren 8955

Description: Equinumerosity relation. (Contributed by NM, 15-Jun-1998.) Extract breng 8954 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 8953	. 2 ⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
2		f1ofn 6834	. . . . 5 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝑓 Fn 𝐴)
3		fndm 6652	. . . . . 6 ⊢ (𝑓 Fn 𝐴 → dom 𝑓 = 𝐴)
4		vex 3477	. . . . . . 7 ⊢ 𝑓 ∈ V
5	4	dmex 7906	. . . . . 6 ⊢ dom 𝑓 ∈ V
6	3, 5	eqeltrrdi 2841	. . . . 5 ⊢ (𝑓 Fn 𝐴 → 𝐴 ∈ V)
7	2, 6	syl 17	. . . 4 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝐴 ∈ V)
8		f1ofo 6840	. . . . . 6 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝑓:𝐴–onto→𝐵)
9		forn 6808	. . . . . 6 ⊢ (𝑓:𝐴–onto→𝐵 → ran 𝑓 = 𝐵)
10	8, 9	syl 17	. . . . 5 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → ran 𝑓 = 𝐵)
11	4	rnex 7907	. . . . 5 ⊢ ran 𝑓 ∈ V
12	10, 11	eqeltrrdi 2841	. . . 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 8954	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴 ≈ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵))
16	1, 14, 15	pm5.21nii 378	1 ⊢ (𝐴 ≈ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵)

Syntax hints:   ↔ wb 205   ∧ wa 395   = wceq 1540  ∃wex 1780   ∈ wcel 2105  Vcvv 3473   class class class wbr 5148  dom cdm 5676  ran crn 5677   Fn wfn 6538  –onto→wfo 6541  –1-1-onto→wf1o 6542   ≈ cen 8942

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702  ax-sep 5299  ax-nul 5306  ax-pr 5427  ax-un 7729

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-ral 3061  df-rex 3070  df-rab 3432  df-v 3475  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-xp 5682  df-rel 5683  df-cnv 5684  df-dm 5686  df-rn 5687  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-en 8946

This theorem is referenced by:  domen  8963  f1oen3g  8968  ener  9003  en0OLD  9020  en0ALT  9021  ensn1OLD  9024  en1OLD  9028  en2snOLD  9048  unen  9052  enfixsn  9087  canth2  9136  mapen  9147  ssenen  9157  rexdif1enOLD  9165  dif1en  9166  dif1enOLD  9168  ssfiALT  9180  ensymfib  9193  entrfil  9194  phplem2  9214  php3  9218  phplem4OLD  9226  php3OLD  9230  isinf  9266  isinfOLD  9267  domunfican  9326  fiint  9330  mapfien2  9410  unxpwdom2  9589  isinffi  9993  infxpenc2  10023  fseqen  10028  dfac8b  10032  infpwfien  10063  dfac12r  10147  infmap2  10219  cff1  10259  infpssr  10309  fin4en1  10310  enfin2i  10322  enfin1ai  10385  axcc3  10439  axcclem  10458  numth  10473  ttukey2g  10517  canthnum  10650  canthwe  10652  canthp1  10655  pwfseq  10665  tskuni  10784  gruen  10813  hasheqf1o  14316  hashfacen  14420  hashfacenOLD  14421  fz1f1o  15663  ruc  16193  cnso  16197  eulerth  16723  ablfaclem3  20005  lbslcic  21707  uvcendim  21713  indishmph  23623  ufldom  23787  ovolctb  25340  ovoliunlem3  25354  iunmbl2  25407  dyadmbl  25450  vitali  25463  cusgrfilem3  29149  padct  32379  f1ocnt  32448  volmeas  33695  eulerpart  33847  derangenlem  34628  mblfinlem1  36992  sticksstones4  41435  sticksstones20  41452  eldioph2lem1  41964  isnumbasgrplem1  42309  nnf1oxpnn  44356  sprsymrelen  46630  prproropen  46638  uspgrspren  46992  uspgrbisymrel  46994  1aryenef  47496  2aryenef  47507  rrx2xpreen  47570