Theorem bren 8993

Description: Equinumerosity relation. (Contributed by NM, 15-Jun-1998.) Extract breng 8992 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 8991	. 2 ⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
2		f1ofn 6849	. . . . 5 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝑓 Fn 𝐴)
3		fndm 6671	. . . . . 6 ⊢ (𝑓 Fn 𝐴 → dom 𝑓 = 𝐴)
4		vex 3481	. . . . . . 7 ⊢ 𝑓 ∈ V
5	4	dmex 7931	. . . . . 6 ⊢ dom 𝑓 ∈ V
6	3, 5	eqeltrrdi 2847	. . . . 5 ⊢ (𝑓 Fn 𝐴 → 𝐴 ∈ V)
7	2, 6	syl 17	. . . 4 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝐴 ∈ V)
8		f1ofo 6855	. . . . . 6 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝑓:𝐴–onto→𝐵)
9		forn 6823	. . . . . 6 ⊢ (𝑓:𝐴–onto→𝐵 → ran 𝑓 = 𝐵)
10	8, 9	syl 17	. . . . 5 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → ran 𝑓 = 𝐵)
11	4	rnex 7932	. . . . 5 ⊢ ran 𝑓 ∈ V
12	10, 11	eqeltrrdi 2847	. . . 4 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝐵 ∈ V)
13	7, 12	jca 511	. . 3 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
14	13	exlimiv 1927	. 2 ⊢ (∃𝑓 𝑓:𝐴–1-1-onto→𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
15		breng 8992	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴 ≈ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵))
16	1, 14, 15	pm5.21nii 378	1 ⊢ (𝐴 ≈ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵)

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1536  ∃wex 1775   ∈ wcel 2105  Vcvv 3477   class class class wbr 5147  dom cdm 5688  ran crn 5689   Fn wfn 6557  –onto→wfo 6560  –1-1-onto→wf1o 6561   ≈ cen 8980

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437  ax-un 7753

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-xp 5694  df-rel 5695  df-cnv 5696  df-dm 5698  df-rn 5699  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-en 8984

This theorem is referenced by:  domen  9000  f1oen3g  9005  ener  9039  en0ALT  9057  unen  9084  enfixsn  9119  canth2  9168  mapen  9179  ssenen  9189  rexdif1enOLD  9197  dif1en  9198  dif1enOLD  9200  ssfiALT  9212  ensymfib  9221  entrfil  9222  phplem2  9242  php3  9246  phplem4OLD  9254  php3OLD  9258  isinf  9293  isinfOLD  9294  domunfican  9358  fiint  9363  fiintOLD  9364  mapfien2  9446  unxpwdom2  9625  isinffi  10029  infxpenc2  10059  fseqen  10064  dfac8b  10068  infpwfien  10099  dfac12r  10184  infmap2  10254  cff1  10295  infpssr  10345  fin4en1  10346  enfin2i  10358  enfin1ai  10421  axcc3  10475  axcclem  10494  numth  10509  ttukey2g  10553  canthnum  10686  canthwe  10688  canthp1  10691  pwfseq  10701  tskuni  10820  gruen  10849  hasheqf1o  14384  hashfacen  14489  fz1f1o  15742  ruc  16275  cnso  16279  eulerth  16816  ablfaclem3  20121  lbslcic  21878  uvcendim  21884  indishmph  23821  ufldom  23985  ovolctb  25538  ovoliunlem3  25552  iunmbl2  25605  dyadmbl  25648  vitali  25661  cusgrfilem3  29489  padct  32736  f1ocnt  32809  volmeas  34211  eulerpart  34363  derangenlem  35155  mblfinlem1  37643  sticksstones4  42130  sticksstones20  42147  eldioph2lem1  42747  isnumbasgrplem1  43089  nnf1oxpnn  45137  sprsymrelen  47424  prproropen  47432  uspgrspren  47995  uspgrbisymrel  47997  1aryenef  48494  2aryenef  48505  rrx2xpreen  48568