Theorem bren 9013

Description: Equinumerosity relation. (Contributed by NM, 15-Jun-1998.) Extract breng 9012 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 9011	. 2 ⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
2		f1ofn 6863	. . . . 5 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝑓 Fn 𝐴)
3		fndm 6682	. . . . . 6 ⊢ (𝑓 Fn 𝐴 → dom 𝑓 = 𝐴)
4		vex 3492	. . . . . . 7 ⊢ 𝑓 ∈ V
5	4	dmex 7949	. . . . . 6 ⊢ dom 𝑓 ∈ V
6	3, 5	eqeltrrdi 2853	. . . . 5 ⊢ (𝑓 Fn 𝐴 → 𝐴 ∈ V)
7	2, 6	syl 17	. . . 4 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝐴 ∈ V)
8		f1ofo 6869	. . . . . 6 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → 𝑓:𝐴–onto→𝐵)
9		forn 6837	. . . . . 6 ⊢ (𝑓:𝐴–onto→𝐵 → ran 𝑓 = 𝐵)
10	8, 9	syl 17	. . . . 5 ⊢ (𝑓:𝐴–1-1-onto→𝐵 → ran 𝑓 = 𝐵)
11	4	rnex 7950	. . . . 5 ⊢ ran 𝑓 ∈ V
12	10, 11	eqeltrrdi 2853	. . . 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 9012	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴 ≈ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵))
16	1, 14, 15	pm5.21nii 378	1 ⊢ (𝐴 ≈ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵)

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1537  ∃wex 1777   ∈ wcel 2108  Vcvv 3488   class class class wbr 5166  dom cdm 5700  ran crn 5701   Fn wfn 6568  –onto→wfo 6571  –1-1-onto→wf1o 6572   ≈ cen 9000

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447  ax-un 7770

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-xp 5706  df-rel 5707  df-cnv 5708  df-dm 5710  df-rn 5711  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-en 9004

This theorem is referenced by:  domen  9021  f1oen3g  9026  ener  9061  en0OLD  9079  en0ALT  9080  ensn1OLD  9083  en1OLD  9087  en2snOLD  9107  unen  9112  enfixsn  9147  canth2  9196  mapen  9207  ssenen  9217  rexdif1enOLD  9225  dif1en  9226  dif1enOLD  9228  ssfiALT  9241  ensymfib  9250  entrfil  9251  phplem2  9271  php3  9275  phplem4OLD  9283  php3OLD  9287  isinf  9323  isinfOLD  9324  domunfican  9389  fiint  9394  fiintOLD  9395  mapfien2  9478  unxpwdom2  9657  isinffi  10061  infxpenc2  10091  fseqen  10096  dfac8b  10100  infpwfien  10131  dfac12r  10216  infmap2  10286  cff1  10327  infpssr  10377  fin4en1  10378  enfin2i  10390  enfin1ai  10453  axcc3  10507  axcclem  10526  numth  10541  ttukey2g  10585  canthnum  10718  canthwe  10720  canthp1  10723  pwfseq  10733  tskuni  10852  gruen  10881  hasheqf1o  14398  hashfacen  14503  fz1f1o  15758  ruc  16291  cnso  16295  eulerth  16830  ablfaclem3  20131  lbslcic  21884  uvcendim  21890  indishmph  23827  ufldom  23991  ovolctb  25544  ovoliunlem3  25558  iunmbl2  25611  dyadmbl  25654  vitali  25667  cusgrfilem3  29493  padct  32733  f1ocnt  32807  volmeas  34195  eulerpart  34347  derangenlem  35139  mblfinlem1  37617  sticksstones4  42106  sticksstones20  42123  eldioph2lem1  42716  isnumbasgrplem1  43058  nnf1oxpnn  45102  sprsymrelen  47374  prproropen  47382  uspgrspren  47875  uspgrbisymrel  47877  1aryenef  48379  2aryenef  48390  rrx2xpreen  48453