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

Theorem brrelex1 5611
Description: If two classes are related by a binary relation, then the first class is a set. (Contributed by NM, 18-May-2004.) (Revised by Mario Carneiro, 26-Apr-2015.)
Assertion
Ref Expression
brrelex1 ((Rel 𝑅𝐴𝑅𝐵) → 𝐴 ∈ V)

Proof of Theorem brrelex1
StepHypRef Expression
1 brrelex12 5610 . 2 ((Rel 𝑅𝐴𝑅𝐵) → (𝐴 ∈ V ∧ 𝐵 ∈ V))
21simpld 498 1 ((Rel 𝑅𝐴𝑅𝐵) → 𝐴 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  wcel 2111  Vcvv 3415   class class class wbr 5062  Rel wrel 5565
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2113  ax-9 2121  ax-ext 2709  ax-sep 5201  ax-nul 5208  ax-pr 5331
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2072  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3067  df-rex 3068  df-rab 3071  df-v 3417  df-dif 3878  df-un 3880  df-in 3882  df-ss 3892  df-nul 4247  df-if 4449  df-sn 4551  df-pr 4553  df-op 4557  df-br 5063  df-opab 5125  df-xp 5566  df-rel 5567
This theorem is referenced by:  brrelex1i  5614  posn  5643  frsn  5645  releldm  5822  relelrn  5823  relimasn  5961  funmo  6405  ertr  8415  dirtr  18121  eqvreltr  36470  frege129d  41063  nnfoctb  42283  clim2d  42904  climfv  42922  meadjiun  43694  caragenunicl  43752
  Copyright terms: Public domain W3C validator