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

Theorem brabga 4904
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 4578 . . 3 (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
2 brabga.2 . . . 4 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}
32eleq2i 2679 . . 3 (⟨𝐴, 𝐵⟩ ∈ 𝑅 ↔ ⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑})
41, 3bitri 262 . 2 (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑})
5 opelopabga.1 . . 3 ((𝑥 = 𝐴𝑦 = 𝐵) → (𝜑𝜓))
65opelopabga 4903 . 2 ((𝐴𝑉𝐵𝑊) → (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜓))
74, 6syl5bb 270 1 ((𝐴𝑉𝐵𝑊) → (𝐴𝑅𝐵𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382   = wceq 1474  wcel 1976  cop 4130   class class class wbr 4577  {copab 4636
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2232  ax-ext 2589  ax-sep 4703  ax-nul 4712  ax-pr 4828
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 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-rab 2904  df-v 3174  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-br 4578  df-opab 4638
This theorem is referenced by:  braba  4907  brabg  4909  epelg  4940  brcog  5198  fmptco  6288  ofrfval  6780  isfsupp  8139  wemaplem1  8311  oemapval  8440  wemapwe  8454  fpwwe2lem2  9310  fpwwelem  9323  clim  14019  rlim  14020  vdwmc  15466  isstruct2  15650  brssc  16243  isfunc  16293  isfull  16339  isfth  16343  ipole  16927  eqgval  17412  frgpuplem  17954  dvdsr  18415  islindf  19912  ulmval  23855  hpgbr  25370  isuhgra  25593  isushgra  25596  isumgra  25610  isuslgra  25638  isusgra  25639  isausgra  25649  iscusgra  25751  iswlkon  25828  istrlon  25837  ispthon  25872  isspthon  25879  isconngra  25966  isconngra1  25967  erclwwlkeq  26105  erclwwlkneq  26117  iseupa  26258  hlimi  27235  isinftm  28872  metidv  29069  ismntoplly  29203  brae  29437  braew  29438  brfae  29444  climf  38493  climf2  38537  isausgr  40396  issubgr  40497  isrgr  40761  isrusgr  40763  istrlson  40916  upgrwlkdvspth  40947  ispthson  40950  isspthson  40951  erclwwlkseq  41241  erclwwlksneq  41253  iscllaw  41617  iscomlaw  41618  isasslaw  41620  islininds  42031  lindepsnlininds  42037
  Copyright terms: Public domain W3C validator