Theorem bren 8941

Description: Equinumerosity relation. (Contributed by NM, 15-Jun-1998.) Extract breng 8940 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 8939	. 2 ⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
2		f1ofn 6811	. . . . 5 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝑓 Fn 𝐴)
3		fndm 6628	. . . . . 6 ⊢ (𝑓 Fn 𝐴 → dom 𝑓 = 𝐴)
4		vex 3461	. . . . . . 7 ⊢ 𝑓 ∈ V
5	4	dmex 7894	. . . . . 6 ⊢ dom 𝑓 ∈ V
6	3, 5	eqeltrrdi 2874	. . . . 5 ⊢ (𝑓 Fn 𝐴 → 𝐴 ∈ V)
7	2, 6	syl 18	. . . 4 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝐴 ∈ V)
8		f1ofo 6818	. . . . . 6 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝑓:𝐴–onto→𝐵)
9		forn 6785	. . . . . 6 ⊢ (𝑓:𝐴–onto→𝐵 → ran 𝑓 = 𝐵)
10	8, 9	syl 18	. . . . 5 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → ran 𝑓 = 𝐵)
11	4	rnex 7895	. . . . 5 ⊢ ran 𝑓 ∈ V
12	10, 11	eqeltrrdi 2874	. . . 4 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝐵 ∈ V)
13	7, 12	jca 520	. . 3 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
14	13	exlimiv 1953	. 2 ⊢ (∃𝑓 𝑓:𝐴–1-1-onto→𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
15		breng 8940	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴 ≈ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵))
16	1, 14, 15	pm5.21nii 381	1 ⊢ (𝐴 ≈ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵)

Syntax hints:   ↔ wb 209   ∧ wa 400   = wceq 1563  ∃wex 1802   ∈ wcel 2145  Vcvv 3457   class class class wbr 5105  dom cdm 5652  ran crn 5653   Fn wfn 6520  –onto→wfo 6523  –1-1-onto→wf1o 6524   ≈ cen 8928

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-sep 5251  ax-pr 5395  ax-un 7722

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-br 5106  df-opab 5168  df-xp 5658  df-rel 5659  df-cnv 5660  df-dm 5662  df-rn 5663  df-fn 6528  df-f 6529  df-f1 6530  df-fo 6531  df-f1o 6532  df-en 8932

This theorem is referenced by:  domen  8946  f1oen3g  8951  ener  8986  en0ALT  9004  unen  9030  enfixsn  9062  canth2  9106  mapen  9117  ssenen  9127  dif1en  9134  ssfiALT  9146  ensymfib  9156  entrfil  9157  phplem2  9177  php3  9181  isinf  9213  domunfican  9269  fiint  9274  mapfien2  9357  unxpwdom2  9538  isinffi  9966  infxpenc2  9994  fseqen  9999  dfac8b  10003  infpwfien  10034  dfac12r  10118  infmap2  10188  cff1  10230  infpssr  10280  fin4en1  10281  enfin2i  10293  enfin1ai  10356  axcc3  10410  axcclem  10429  numth  10444  ttukey2g  10488  canthnum  10622  canthwe  10624  canthp1  10627  pwfseq  10637  tskuni  10756  gruen  10785  hasheqf1o  14376  hashfacen  14481  fz1f1o  15751  ruc  16289  cnso  16293  eulerth  16832  ablfaclem3  20150  lbslcic  21951  uvcendim  21957  indishmph  23916  ufldom  24080  ovolctb  25610  ovoliunlem3  25624  iunmbl2  25677  dyadmbl  25720  vitali  25733  cusgrfilem3  29716  padct  32975  f1ocnt  33057  volmeas  34538  eulerpart  34689  derangenlem  35534  mblfinlem1  38168  sticksstones4  42778  sticksstones20  42795  eldioph2lem1  43353  isnumbasgrplem1  43690  nnf1oxpnn  45771  sprsymrelen  48104  prproropen  48112  uspgrspren  48772  uspgrbisymrel  48774  1aryenef  49276  2aryenef  49287  rrx2xpreen  49350