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

Theorem brab 5542
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 5538 . 2 ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴𝑅𝐵𝜒))
71, 2, 6mp2an 690 1 (𝐴𝑅𝐵𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205   = wceq 1541  wcel 2106  Vcvv 3474   class class class wbr 5147  {copab 5209
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pr 5426
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-br 5148  df-opab 5210
This theorem is referenced by:  opbrop  5771  f1oweALT  7955  frxp  8108  fnwelem  8113  xpord2lem  8124  xpord3lem  8131  poseq  8140  dftpos4  8226  dfac3  10112  axdc2lem  10439  brdom7disj  10522  brdom6disj  10523  ordpipq  10933  ltresr  11131  shftfn  15016  2shfti  15023  ishpg  27999  brcgr  28147  ex-opab  29674  br8d  31826  br8  34714  br6  34715  br4  34716  dfbigcup2  34859  brsegle  35068  heiborlem2  36668
  Copyright terms: Public domain W3C validator