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

Theorem brrelex12 5295
Description: A true binary relation on a relation implies the arguments are sets. (This is a property of our ordered pair definition.) (Contributed by Mario Carneiro, 26-Apr-2015.)
Assertion
Ref Expression
brrelex12 ((Rel 𝑅𝐴𝑅𝐵) → (𝐴 ∈ V ∧ 𝐵 ∈ V))

Proof of Theorem brrelex12
StepHypRef Expression
1 df-rel 5256 . . . . 5 (Rel 𝑅𝑅 ⊆ (V × V))
21biimpi 206 . . . 4 (Rel 𝑅𝑅 ⊆ (V × V))
32ssbrd 4827 . . 3 (Rel 𝑅 → (𝐴𝑅𝐵𝐴(V × V)𝐵))
43imp 393 . 2 ((Rel 𝑅𝐴𝑅𝐵) → 𝐴(V × V)𝐵)
5 brxp 5287 . 2 (𝐴(V × V)𝐵 ↔ (𝐴 ∈ V ∧ 𝐵 ∈ V))
64, 5sylib 208 1 ((Rel 𝑅𝐴𝑅𝐵) → (𝐴 ∈ V ∧ 𝐵 ∈ V))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  wcel 2144  Vcvv 3349  wss 3721   class class class wbr 4784   × cxp 5247  Rel wrel 5254
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750  ax-sep 4912  ax-nul 4920  ax-pr 5034
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3an 1072  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-ral 3065  df-rex 3066  df-rab 3069  df-v 3351  df-dif 3724  df-un 3726  df-in 3728  df-ss 3735  df-nul 4062  df-if 4224  df-sn 4315  df-pr 4317  df-op 4321  df-br 4785  df-opab 4845  df-xp 5255  df-rel 5256
This theorem is referenced by:  brrelex  5296  brrelex2  5297  nprrel12  5300  relbrcnvg  5645  ovprc  6827  oprabv  6849  brovex  7499  ersym  7907  relelec  7938  encv  8116  fsuppunbi  8451  fpwwe2lem2  9655  fpwwelem  9668  brfi1uzind  13481  isstruct2  16073  brssc  16680  cofuval2  16753  isfull  16776  isfth  16780  isnat  16813  pslem  17413  frgpuplem  18391  dvdsr  18853  ulmval  24353  perpln1  25825  perpln2  25826  opelco3  32008  rngoablo2  34033  aovprc  41782  aovrcl  41783  nelbrim  41809
  Copyright terms: Public domain W3C validator