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

Theorem brdomi 8954
Description: Dominance relation. (Contributed by Mario Carneiro, 26-Apr-2015.) Avoid ax-un 7725. (Revised by BTernaryTau, 29-Nov-2024.)
Assertion
Ref Expression
brdomi (𝐴𝐵 → ∃𝑓 𝑓:𝐴1-1𝐵)
Distinct variable groups:   𝐴,𝑓   𝐵,𝑓

Proof of Theorem brdomi
StepHypRef Expression
1 reldom 8945 . . . 4 Rel ≼
21brrelex12i 5732 . . 3 (𝐴𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
3 brdom2g 8951 . . 3 ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴𝐵 ↔ ∃𝑓 𝑓:𝐴1-1𝐵))
42, 3syl 17 . 2 (𝐴𝐵 → (𝐴𝐵 ↔ ∃𝑓 𝑓:𝐴1-1𝐵))
54ibi 267 1 (𝐴𝐵 → ∃𝑓 𝑓:𝐴1-1𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397  wex 1782  wcel 2107  Vcvv 3475   class class class wbr 5149  1-1wf1 6541  cdom 8937
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150  df-opab 5212  df-xp 5683  df-rel 5684  df-fn 6547  df-f 6548  df-f1 6549  df-dom 8941
This theorem is referenced by:  domssl  8994  domssr  8995  2dom  9030  undom  9059  xpdom2  9067  domunsncan  9072  sucdom2OLD  9082  dom0  9102  fodomr  9128  domssex  9138  domtrfil  9195  sucdom2  9206  sdom1  9242  1sdom2dom  9247  infn0  9307  hartogslem1  9537  infdifsn  9652  acndom  10046  acndom2  10049  fictb  10240  fin23lem41  10347  iundom2g  10535  pwfseq  10659  omssubadd  33330
  Copyright terms: Public domain W3C validator