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

Theorem brabga 5447
Description: The law of concretion for a binary relation. (Contributed by Mario Carneiro, 19-Dec-2013.)
Hypotheses
Ref Expression
opelopabga.1 ((𝑥 = 𝐴𝑦 = 𝐵) → (𝜑𝜓))
brabga.2 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}
Assertion
Ref Expression
brabga ((𝐴𝑉𝐵𝑊) → (𝐴𝑅𝐵𝜓))
Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦   𝜓,𝑥,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝑅(𝑥,𝑦)   𝑉(𝑥,𝑦)   𝑊(𝑥,𝑦)

Proof of Theorem brabga
StepHypRef Expression
1 df-br 5075 . . 3 (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
2 brabga.2 . . . 4 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}
32eleq2i 2830 . . 3 (⟨𝐴, 𝐵⟩ ∈ 𝑅 ↔ ⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑})
41, 3bitri 274 . 2 (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑})
5 opelopabga.1 . . 3 ((𝑥 = 𝐴𝑦 = 𝐵) → (𝜑𝜓))
65opelopabga 5446 . 2 ((𝐴𝑉𝐵𝑊) → (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜓))
74, 6bitrid 282 1 ((𝐴𝑉𝐵𝑊) → (𝐴𝑅𝐵𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1539  wcel 2106  cop 4567   class class class wbr 5074  {copab 5136
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-br 5075  df-opab 5137
This theorem is referenced by:  braba  5450  brabg  5452  epelg  5496  brcog  5775  fmptco  7001  ofrfvalg  7541  isfsupp  9132  wemaplem1  9305  oemapval  9441  wemapwe  9455  fpwwe2lem2  10388  fpwwelem  10401  clim  15203  rlim  15204  vdwmc  16679  isstruct2  16850  brssc  17526  isfunc  17579  isfull  17626  isfth  17630  ipole  18252  eqgval  18805  frgpuplem  19378  dvdsr  19888  islindf  21019  ulmval  25539  hpgbr  27121  isausgr  27534  issubgr  27638  isrgr  27926  isrusgr  27928  istrlson  28075  upgrwlkdvspth  28107  ispthson  28110  isspthson  28111  erclwwlkeq  28382  erclwwlkneq  28431  hlimi  29550  isinftm  31435  brfldext  31722  brfinext  31728  metidv  31842  ismntoplly  31975  brae  32209  braew  32210  brfae  32216  satfbrsuc  33328  prv  33390  bj-epelg  35239  bj-ideqgALT  35329  bj-idreseq  35333  bj-idreseqb  35334  bj-ideqg1ALT  35336  brcoss  36554  brcoels  36558  brdmqss  36759  climf  43163  climf2  43207  nelbr  44766  isomgr  45275  iscllaw  45383  iscomlaw  45384  isasslaw  45386  islininds  45787  lindepsnlininds  45793
  Copyright terms: Public domain W3C validator