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

Theorem brabga 5390
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 5032 . . 3 (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
2 brabga.2 . . . 4 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}
32eleq2i 2825 . . 3 (⟨𝐴, 𝐵⟩ ∈ 𝑅 ↔ ⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑})
41, 3bitri 278 . 2 (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑})
5 opelopabga.1 . . 3 ((𝑥 = 𝐴𝑦 = 𝐵) → (𝜑𝜓))
65opelopabga 5389 . 2 ((𝐴𝑉𝐵𝑊) → (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜓))
74, 6syl5bb 286 1 ((𝐴𝑉𝐵𝑊) → (𝐴𝑅𝐵𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399   = wceq 1542  wcel 2114  cop 4523   class class class wbr 5031  {copab 5093
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2711  ax-sep 5168  ax-nul 5175  ax-pr 5297
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2075  df-clab 2718  df-cleq 2731  df-clel 2812  df-v 3401  df-dif 3847  df-un 3849  df-nul 4213  df-if 4416  df-sn 4518  df-pr 4520  df-op 4524  df-br 5032  df-opab 5094
This theorem is referenced by:  braba  5393  brabg  5395  epelg  5436  brcog  5710  fmptco  6904  ofrfvalg  7435  isfsupp  8913  wemaplem1  9086  oemapval  9222  wemapwe  9236  fpwwe2lem2  10135  fpwwelem  10148  clim  14944  rlim  14945  vdwmc  16417  isstruct2  16599  brssc  17192  isfunc  17242  isfull  17288  isfth  17292  ipole  17887  eqgval  18450  frgpuplem  19019  dvdsr  19521  islindf  20631  ulmval  25130  hpgbr  26709  isausgr  27112  issubgr  27216  isrgr  27504  isrusgr  27506  istrlson  27651  upgrwlkdvspth  27683  ispthson  27686  isspthson  27687  erclwwlkeq  27958  erclwwlkneq  28007  hlimi  29126  isinftm  31015  brfldext  31297  brfinext  31303  metidv  31417  ismntoplly  31548  brae  31782  braew  31783  brfae  31789  satfbrsuc  32902  prv  32964  bj-epelg  34884  bj-ideqgALT  34973  bj-idreseq  34977  bj-idreseqb  34978  bj-ideqg1ALT  34980  brcoss  36200  brcoels  36204  brdmqss  36405  climf  42728  climf2  42772  nelbr  44329  isomgr  44839  iscllaw  44947  iscomlaw  44948  isasslaw  44950  islininds  45351  lindepsnlininds  45357
  Copyright terms: Public domain W3C validator