Theorem bren 8967

Description: Equinumerosity relation. (Contributed by NM, 15-Jun-1998.) Extract breng 8966 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 8965	. 2 ⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
2		f1ofn 6817	. . . . 5 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝑓 Fn 𝐴)
3		fndm 6634	. . . . . 6 ⊢ (𝑓 Fn 𝐴 → dom 𝑓 = 𝐴)
4		vex 3455	. . . . . . 7 ⊢ 𝑓 ∈ V
5	4	dmex 7910	. . . . . 6 ⊢ dom 𝑓 ∈ V
6	3, 5	eqeltrrdi 2870	. . . . 5 ⊢ (𝑓 Fn 𝐴 → 𝐴 ∈ V)
7	2, 6	syl 18	. . . 4 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝐴 ∈ V)
8		f1ofo 6824	. . . . . 6 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝑓:𝐴–onto→𝐵)
9		forn 6791	. . . . . 6 ⊢ (𝑓:𝐴–onto→𝐵 → ran 𝑓 = 𝐵)
10	8, 9	syl 18	. . . . 5 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → ran 𝑓 = 𝐵)
11	4	rnex 7911	. . . . 5 ⊢ ran 𝑓 ∈ V
12	10, 11	eqeltrrdi 2870	. . . 4 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝐵 ∈ V)
13	7, 12	jca 521	. . 3 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
14	13	exlimiv 1963	. 2 ⊢ (∃𝑓 𝑓:𝐴–1-1-onto→𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
15		breng 8966	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴 ≈ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵))
16	1, 14, 15	pm5.21nii 381	1 ⊢ (𝐴 ≈ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵)

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   = wceq 1570  ∃wex 1812   ∈ wcel 2145  Vcvv 3451   class class class wbr 5103  dom cdm 5651  ran crn 5652   Fn wfn 6526  –onto→wfo 6529  –1-1-onto→wf1o 6530   ≈ cen 8954

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pr 5391  ax-un 7740

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-xp 5657  df-rel 5658  df-cnv 5659  df-dm 5661  df-rn 5662  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-en 8958

This theorem is used by:  domen  8972  f1oen3g  8977  ener  9012  en0ALT  9030  unen  9057  enfixsn  9089  canth2  9133  mapen  9144  ssenen  9154  dif1en  9161  ssfiALT  9173  ensymfib  9183  entrfil  9184  phplem2  9204  php3  9208  isinf  9240  domunfican  9297  fiint  9302  mapfien2  9385  unxpwdom2  9566  isinffi  10054  infxpenc2  10082  fseqen  10087  dfac8b  10091  infpwfien  10122  dfac12r  10206  infmap2  10276  cff1  10317  infpssr  10367  fin4en1  10368  enfin2i  10380  enfin1ai  10443  axcc3  10497  axcclem  10516  numth  10531  ttukey2g  10575  canthnum  10715  canthwe  10717  canthp1  10720  pwfseq  10730  tskuni  10849  gruen  10878  hasheqf1o  14473  hashfacen  14579  fz1f1o  15856  ruc  16391  cnso  16395  eulerth  16940  ablfaclem3  20283  lbslcic  22127  uvcendim  22133  indishmph  24097  ufldom  24261  ovolctb  25791  ovoliunlem3  25805  iunmbl2  25858  dyadmbl  25901  vitali  25914  cusgrfilem3  30020  padct  33292  f1ocnt  33374  volmeas  34846  eulerpart  34997  derangenlem  35905  mblfinlem1  38543  sticksstones4  43167  sticksstones20  43184  eldioph2lem1  43724  isnumbasgrplem1  44061  nnf1oxpnn  46153  sprsymrelen  48526  prproropen  48534  uspgrspren  49194  uspgrbisymrel  49196  1aryenef  49701  2aryenef  49712  rrx2xpreen  49775