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

Theorem brabga 5544
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 5149 . . 3 (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
2 brabga.2 . . . 4 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}
32eleq2i 2831 . . 3 (⟨𝐴, 𝐵⟩ ∈ 𝑅 ↔ ⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑})
41, 3bitri 275 . 2 (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑})
5 opelopabga.1 . . 3 ((𝑥 = 𝐴𝑦 = 𝐵) → (𝜑𝜓))
65opelopabga 5543 . 2 ((𝐴𝑉𝐵𝑊) → (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜓))
74, 6bitrid 283 1 ((𝐴𝑉𝐵𝑊) → (𝐴𝑅𝐵𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1537  wcel 2106  cop 4637   class class class wbr 5148  {copab 5210
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-br 5149  df-opab 5211
This theorem is referenced by:  braba  5547  brabg  5549  epelg  5590  brcog  5880  fmptco  7149  ofrfvalg  7705  isfsupp  9403  wemaplem1  9584  oemapval  9721  wemapwe  9735  fpwwe2lem2  10670  fpwwelem  10683  clim  15527  rlim  15528  vdwmc  17012  isstruct2  17183  brssc  17862  isfunc  17915  isfull  17964  isfth  17968  ipole  18592  eqgval  19208  frgpuplem  19805  dvdsr  20379  islindf  21850  ulmval  26438  hpgbr  28783  isausgr  29196  issubgr  29303  isrgr  29592  isrusgr  29594  istrlson  29740  upgrwlkdvspth  29772  ispthson  29775  isspthson  29776  erclwwlkeq  30047  erclwwlkneq  30096  hlimi  31217  isinftm  33171  brfldext  33675  brfinext  33681  fldext2chn  33734  metidv  33853  ismntoplly  33988  brae  34222  braew  34223  brfae  34229  satfbrsuc  35351  prv  35413  bj-epelg  37051  bj-ideqgALT  37141  bj-idreseq  37145  bj-idreseqb  37146  bj-ideqg1ALT  37148  brcoss  38413  brcoels  38417  brdmqss  38628  aks6d1c1p1  42089  climf  45578  climf2  45622  nelbr  47224  iscllaw  48033  iscomlaw  48034  isasslaw  48036  islininds  48292  lindepsnlininds  48298
  Copyright terms: Public domain W3C validator