Theorem brabga 5479

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

Step	Hyp	Ref	Expression
1		df-br 5076	. . 3 ⊢ (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
2		brabga.2	. . . 4 ⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}
3	2	eleq2i 2833	. . 3 ⊢ (⟨𝐴, 𝐵⟩ ∈ 𝑅 ↔ ⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑})
4	1, 3	bitri 277	. 2 ⊢ (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑})
5		opelopabga.1	. . 3 ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓))
6	5	opelopabga 5478	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜓))
7	4, 6	bitrid 285	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴𝑅𝐵 ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 397   = wceq 1548   ∈ wcel 2121  ⟨cop 4564   class class class wbr 5075  {copab 5137

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713  ax-sep 5221  ax-pr 5365

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-rab 3394  df-v 3435  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4265  df-if 4458  df-sn 4559  df-pr 4561  df-op 4565  df-br 5076  df-opab 5138

This theorem is referenced by:  braba  5482  brabg  5484  epelg  5522  brcog  5811  fmptco  7075  ofrfvalg  7632  isfsupp  9272  wemaplem1  9455  oemapval  9599  wemapwe  9613  fpwwe2lem2  10550  fpwwelem  10563  clim  15451  rlim  15452  vdwmc  16944  isstruct2  17114  brssc  17776  isfunc  17826  isfull  17874  isfth  17878  ipole  18495  eqgval  19147  frgpuplem  19742  dvdsr  20337  islindf  21791  ulmval  26367  hpgbr  28850  isausgr  29255  issubgr  29362  isrgr  29650  isrusgr  29652  istrlson  29795  upgrwlkdvspth  29829  ispthson  29832  isspthson  29833  erclwwlkeq  30110  erclwwlkneq  30159  hlimi  31281  isinftm  33266  brfldext  33841  brfinext  33848  finextfldext  33860  bralgext  33893  fldext2chn  33924  constrextdg2lem  33944  metidv  34088  ismntoplly  34221  brae  34437  braew  34438  brfae  34444  satfbrsuc  35609  prv  35671  bj-epelg  37436  bj-ideqgALT  37533  bj-idreseq  37537  bj-idreseqb  37538  bj-ideqg1ALT  37540  ecqmap  38831  brsucmap  38848  brcoss  38903  brcoels  38907  brdmqss  39112  aks6d1c1p1  42607  climf  46081  climf2  46123  nelbr  47751  iscllaw  48694  iscomlaw  48695  isasslaw  48697  islininds  48951  lindepsnlininds  48957