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

Theorem brabg 5545
Description: The law of concretion for a binary relation. (Contributed by NM, 16-Aug-1999.) (Revised by Mario Carneiro, 19-Dec-2013.)
Hypotheses
Ref Expression
opelopabg.1 (𝑥 = 𝐴 → (𝜑𝜓))
opelopabg.2 (𝑦 = 𝐵 → (𝜓𝜒))
brabg.5 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}
Assertion
Ref Expression
brabg ((𝐴𝐶𝐵𝐷) → (𝐴𝑅𝐵𝜒))
Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦   𝜒,𝑥,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑥,𝑦)   𝐶(𝑥,𝑦)   𝐷(𝑥,𝑦)   𝑅(𝑥,𝑦)

Proof of Theorem brabg
StepHypRef Expression
1 opelopabg.1 . . 3 (𝑥 = 𝐴 → (𝜑𝜓))
2 opelopabg.2 . . 3 (𝑦 = 𝐵 → (𝜓𝜒))
31, 2sylan9bb 508 . 2 ((𝑥 = 𝐴𝑦 = 𝐵) → (𝜑𝜒))
4 brabg.5 . 2 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}
53, 4brabga 5540 1 ((𝐴𝐶𝐵𝐷) → (𝐴𝑅𝐵𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394   = wceq 1534  wcel 2099   class class class wbr 5153  {copab 5215
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697  ax-sep 5304  ax-nul 5311  ax-pr 5433
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-rab 3420  df-v 3464  df-dif 3950  df-un 3952  df-ss 3964  df-nul 4326  df-if 4534  df-sn 4634  df-pr 4636  df-op 4640  df-br 5154  df-opab 5216
This theorem is referenced by:  brab  5549  ideqg  5858  brcnvg  5886  f1owe  7365  brrpssg  7736  soseq  8173  breng  8983  brenOLD  8985  brdom2g  8986  brdomgOLD  8988  brwdom  9610  brttrcl  9756  ltprord  11073  shftfib  15077  efgrelexlema  19747  isref  23504  sltval  27677  brsslt  27815  lrrecval  27953  istrkgld  28386  islnopp  28666  axcontlem5  28902  cmbr  31517  leopg  32055  cvbr  32215  mdbr  32227  dmdbr  32232  isfne  36051  brabg2  37418  isriscg  37685  brssr  38199  lcvbr  38719  bropabg  42989
  Copyright terms: Public domain W3C validator