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

Theorem brrelex12 5448
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 5408 . . . . 5 (Rel 𝑅𝑅 ⊆ (V × V))
21biimpi 208 . . . 4 (Rel 𝑅𝑅 ⊆ (V × V))
32ssbrd 4966 . . 3 (Rel 𝑅 → (𝐴𝑅𝐵𝐴(V × V)𝐵))
43imp 398 . 2 ((Rel 𝑅𝐴𝑅𝐵) → 𝐴(V × V)𝐵)
5 brxp 5447 . 2 (𝐴(V × V)𝐵 ↔ (𝐴 ∈ V ∧ 𝐵 ∈ V))
64, 5sylib 210 1 ((Rel 𝑅𝐴𝑅𝐵) → (𝐴 ∈ V ∧ 𝐵 ∈ V))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 387  wcel 2050  Vcvv 3409  wss 3823   class class class wbr 4923   × cxp 5399  Rel wrel 5406
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-ext 2744  ax-sep 5054  ax-nul 5061  ax-pr 5180
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2753  df-cleq 2765  df-clel 2840  df-nfc 2912  df-ral 3087  df-rex 3088  df-rab 3091  df-v 3411  df-dif 3826  df-un 3828  df-in 3830  df-ss 3837  df-nul 4173  df-if 4345  df-sn 4436  df-pr 4438  df-op 4442  df-br 4924  df-opab 4986  df-xp 5407  df-rel 5408
This theorem is referenced by:  brrelex1  5449  brrelex2  5450  brrelex12i  5451  relbrcnvg  5802  brovex  7685  ersym  8095  relelec  8128  fpwwe2lem2  9846  fpwwelem  9859  cofuval2  17009  isnat  17069  pslem  17668  frgpuplem  18652  perpln1  26192  perpln2  26193  poprelb  43054
  Copyright terms: Public domain W3C validator