MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  bren Structured version   Visualization version   GIF version

Theorem bren 8826
Description: Equinumerosity relation. (Contributed by NM, 15-Jun-1998.) Extract breng 8825 as an intermediate result. (Revised by BTernaryTau, 23-Sep-2024.)
Assertion
Ref Expression
bren (𝐴𝐵 ↔ ∃𝑓 𝑓:𝐴1-1-onto𝐵)
Distinct variable groups:   𝐴,𝑓   𝐵,𝑓

Proof of Theorem bren
StepHypRef Expression
1 encv 8824 . 2 (𝐴𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
2 f1ofn 6780 . . . . 5 (𝑓:𝐴1-1-onto𝐵𝑓 Fn 𝐴)
3 fndm 6600 . . . . . 6 (𝑓 Fn 𝐴 → dom 𝑓 = 𝐴)
4 vex 3447 . . . . . . 7 𝑓 ∈ V
54dmex 7838 . . . . . 6 dom 𝑓 ∈ V
63, 5eqeltrrdi 2847 . . . . 5 (𝑓 Fn 𝐴𝐴 ∈ V)
72, 6syl 17 . . . 4 (𝑓:𝐴1-1-onto𝐵𝐴 ∈ V)
8 f1ofo 6786 . . . . . 6 (𝑓:𝐴1-1-onto𝐵𝑓:𝐴onto𝐵)
9 forn 6754 . . . . . 6 (𝑓:𝐴onto𝐵 → ran 𝑓 = 𝐵)
108, 9syl 17 . . . . 5 (𝑓:𝐴1-1-onto𝐵 → ran 𝑓 = 𝐵)
114rnex 7839 . . . . 5 ran 𝑓 ∈ V
1210, 11eqeltrrdi 2847 . . . 4 (𝑓:𝐴1-1-onto𝐵𝐵 ∈ V)
137, 12jca 512 . . 3 (𝑓:𝐴1-1-onto𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
1413exlimiv 1933 . 2 (∃𝑓 𝑓:𝐴1-1-onto𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
15 breng 8825 . 2 ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴𝐵 ↔ ∃𝑓 𝑓:𝐴1-1-onto𝐵))
161, 14, 15pm5.21nii 379 1 (𝐴𝐵 ↔ ∃𝑓 𝑓:𝐴1-1-onto𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 396   = wceq 1541  wex 1781  wcel 2106  Vcvv 3443   class class class wbr 5103  dom cdm 5630  ran crn 5631   Fn wfn 6486  ontowfo 6489  1-1-ontowf1o 6490  cen 8813
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2708  ax-sep 5254  ax-nul 5261  ax-pr 5382  ax-un 7662
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-ral 3063  df-rex 3072  df-rab 3406  df-v 3445  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4281  df-if 4485  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4864  df-br 5104  df-opab 5166  df-xp 5636  df-rel 5637  df-cnv 5638  df-dm 5640  df-rn 5641  df-fn 6494  df-f 6495  df-f1 6496  df-fo 6497  df-f1o 6498  df-en 8817
This theorem is referenced by:  domen  8834  f1oen3g  8839  ener  8874  en0OLD  8891  en0ALT  8892  ensn1OLD  8895  en1OLD  8899  en2snOLD  8919  unen  8923  enfixsn  8958  canth2  9007  mapen  9018  ssenen  9028  rexdif1enOLD  9036  dif1en  9037  dif1enOLD  9039  ssfiALT  9051  ensymfib  9064  entrfil  9065  phplem2  9085  php3  9089  phplem4OLD  9097  php3OLD  9101  isinf  9137  isinfOLD  9138  domunfican  9197  fiint  9201  mapfien2  9278  unxpwdom2  9457  isinffi  9861  infxpenc2  9891  fseqen  9896  dfac8b  9900  infpwfien  9931  dfac12r  10015  infmap2  10087  cff1  10127  infpssr  10177  fin4en1  10178  enfin2i  10190  enfin1ai  10253  axcc3  10307  axcclem  10326  numth  10341  ttukey2g  10385  canthnum  10518  canthwe  10520  canthp1  10523  pwfseq  10533  tskuni  10652  gruen  10681  hasheqf1o  14176  hashfacen  14278  hashfacenOLD  14279  fz1f1o  15529  ruc  16059  cnso  16063  eulerth  16589  ablfaclem3  19795  lbslcic  21170  uvcendim  21176  indishmph  23071  ufldom  23235  ovolctb  24776  ovoliunlem3  24790  iunmbl2  24843  dyadmbl  24886  vitali  24899  cusgrfilem3  28203  padct  31430  f1ocnt  31499  volmeas  32603  eulerpart  32755  derangenlem  33538  mblfinlem1  36010  sticksstones4  40452  sticksstones20  40469  eldioph2lem1  40948  isnumbasgrplem1  41293  nnf1oxpnn  43172  sprsymrelen  45441  prproropen  45449  uspgrspren  45803  uspgrbisymrel  45805  1aryenef  46480  2aryenef  46491  rrx2xpreen  46554
  Copyright terms: Public domain W3C validator