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

Theorem brab 5481
Description: The law of concretion for a binary relation. (Contributed by NM, 16-Aug-1999.)
Hypotheses
Ref Expression
opelopab.1 𝐴 ∈ V
opelopab.2 𝐵 ∈ V
opelopab.3 (𝑥 = 𝐴 → (𝜑𝜓))
opelopab.4 (𝑦 = 𝐵 → (𝜓𝜒))
brab.5 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}
Assertion
Ref Expression
brab (𝐴𝑅𝐵𝜒)
Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦   𝜒,𝑥,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑥,𝑦)   𝑅(𝑥,𝑦)

Proof of Theorem brab
StepHypRef Expression
1 opelopab.1 . 2 𝐴 ∈ V
2 opelopab.2 . 2 𝐵 ∈ V
3 opelopab.3 . . 3 (𝑥 = 𝐴 → (𝜑𝜓))
4 opelopab.4 . . 3 (𝑦 = 𝐵 → (𝜓𝜒))
5 brab.5 . . 3 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}
63, 4, 5brabg 5477 . 2 ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴𝑅𝐵𝜒))
71, 2, 6mp2an 689 1 (𝐴𝑅𝐵𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205   = wceq 1540  wcel 2105  Vcvv 3441   class class class wbr 5089  {copab 5151
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707  ax-sep 5240  ax-nul 5247  ax-pr 5369
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-rab 3404  df-v 3443  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4269  df-if 4473  df-sn 4573  df-pr 4575  df-op 4579  df-br 5090  df-opab 5152
This theorem is referenced by:  opbrop  5709  f1oweALT  7875  frxp  8026  fnwelem  8031  poseq  8037  dftpos4  8123  dfac3  9970  axdc2lem  10297  brdom7disj  10380  brdom6disj  10381  ordpipq  10791  ltresr  10989  shftfn  14875  2shfti  14882  ishpg  27350  brcgr  27498  ex-opab  29025  br8d  31178  br8  33956  br6  33957  br4  33958  xpord2lem  34015  xpord3lem  34021  dfbigcup2  34292  brsegle  34501  heiborlem2  36068
  Copyright terms: Public domain W3C validator