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

Theorem brabga 4808
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 4482 . . 3 (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
2 brabga.2 . . . 4 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}
32eleq2i 2584 . . 3 (⟨𝐴, 𝐵⟩ ∈ 𝑅 ↔ ⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑})
41, 3bitri 262 . 2 (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑})
5 opelopabga.1 . . 3 ((𝑥 = 𝐴𝑦 = 𝐵) → (𝜑𝜓))
65opelopabga 4807 . 2 ((𝐴𝑉𝐵𝑊) → (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜓))
74, 6syl5bb 270 1 ((𝐴𝑉𝐵𝑊) → (𝐴𝑅𝐵𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382   = wceq 1474  wcel 1938  cop 4034   class class class wbr 4481  {copab 4540
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-9 1947  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494  ax-sep 4607  ax-nul 4616  ax-pr 4732
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1699  df-sb 1831  df-eu 2366  df-mo 2367  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-rab 2809  df-v 3079  df-dif 3447  df-un 3449  df-in 3451  df-ss 3458  df-nul 3778  df-if 3940  df-sn 4029  df-pr 4031  df-op 4035  df-br 4482  df-opab 4542
This theorem is referenced by:  braba  4811  brabg  4813  epelg  4844  brcog  5102  fmptco  6192  ofrfval  6684  isfsupp  8042  wemaplem1  8214  oemapval  8343  wemapwe  8357  fpwwe2lem2  9213  fpwwelem  9226  clim  13943  rlim  13944  vdwmc  15408  isstruct2  15592  brssc  16193  isfunc  16243  isfull  16289  isfth  16293  ipole  16877  eqgval  17362  frgpuplem  17920  dvdsr  18380  islindf  19877  ulmval  23829  hpgbr  25346  isuhgra  25569  isushgra  25572  isumgra  25586  isuslgra  25614  isusgra  25615  isausgra  25625  iscusgra  25727  iswlkon  25804  istrlon  25813  ispthon  25848  isspthon  25855  isconngra  25942  isconngra1  25943  erclwwlkeq  26081  erclwwlkneq  26093  iseupa  26234  hlimi  27221  isinftm  28866  metidv  29063  ismntoplly  29197  brae  29431  braew  29432  brfae  29438  climf  38592  climf2  38637  isausgr  40503  issubgr  40604  isrgr  40868  isrusgr  40870  istrlson  41023  upgrwlkdvspth  41054  ispthson  41057  isspthson  41058  erclwwlkseq  41348  erclwwlksneq  41360  iscllaw  41724  iscomlaw  41725  isasslaw  41727  islininds  42138  lindepsnlininds  42144
  Copyright terms: Public domain W3C validator