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

Theorem brabga 5536
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 5150 . . 3 (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
2 brabga.2 . . . 4 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}
32eleq2i 2817 . . 3 (⟨𝐴, 𝐵⟩ ∈ 𝑅 ↔ ⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑})
41, 3bitri 274 . 2 (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑})
5 opelopabga.1 . . 3 ((𝑥 = 𝐴𝑦 = 𝐵) → (𝜑𝜓))
65opelopabga 5535 . 2 ((𝐴𝑉𝐵𝑊) → (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜓))
74, 6bitrid 282 1 ((𝐴𝑉𝐵𝑊) → (𝐴𝑅𝐵𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394   = wceq 1533  wcel 2098  cop 4636   class class class wbr 5149  {copab 5211
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696  ax-sep 5300  ax-nul 5307  ax-pr 5429
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-rab 3419  df-v 3463  df-dif 3947  df-un 3949  df-ss 3961  df-nul 4323  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5150  df-opab 5212
This theorem is referenced by:  braba  5539  brabg  5541  epelg  5583  brcog  5869  fmptco  7138  ofrfvalg  7693  isfsupp  9391  wemaplem1  9571  oemapval  9708  wemapwe  9722  fpwwe2lem2  10657  fpwwelem  10670  clim  15474  rlim  15475  vdwmc  16950  isstruct2  17121  brssc  17800  isfunc  17853  isfull  17902  isfth  17906  ipole  18529  eqgval  19140  frgpuplem  19739  dvdsr  20313  islindf  21763  ulmval  26361  hpgbr  28636  isausgr  29049  issubgr  29156  isrgr  29445  isrusgr  29447  istrlson  29593  upgrwlkdvspth  29625  ispthson  29628  isspthson  29629  erclwwlkeq  29900  erclwwlkneq  29949  hlimi  31070  isinftm  32981  brfldext  33470  brfinext  33476  metidv  33624  ismntoplly  33757  brae  33991  braew  33992  brfae  33998  satfbrsuc  35107  prv  35169  bj-epelg  36678  bj-ideqgALT  36768  bj-idreseq  36772  bj-idreseqb  36773  bj-ideqg1ALT  36775  brcoss  38033  brcoels  38037  brdmqss  38248  aks6d1c1p1  41710  climf  45148  climf2  45192  nelbr  46792  iscllaw  47437  iscomlaw  47438  isasslaw  47440  islininds  47700  lindepsnlininds  47706
  Copyright terms: Public domain W3C validator