Theorem brabga 5480

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 5097	. . 3 ⊢ (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
2		brabga.2	. . . 4 ⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}
3	2	eleq2i 2826	. . 3 ⊢ (⟨𝐴, 𝐵⟩ ∈ 𝑅 ↔ ⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑})
4	1, 3	bitri 275	. 2 ⊢ (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑})
5		opelopabga.1	. . 3 ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓))
6	5	opelopabga 5479	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜓))
7	4, 6	bitrid 283	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴𝑅𝐵 ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2113  ⟨cop 4584   class class class wbr 5096  {copab 5158

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-br 5097  df-opab 5159

This theorem is referenced by:  braba  5483  brabg  5485  epelg  5523  brcog  5813  fmptco  7072  ofrfvalg  7628  isfsupp  9266  wemaplem1  9449  oemapval  9590  wemapwe  9604  fpwwe2lem2  10541  fpwwelem  10554  clim  15415  rlim  15416  vdwmc  16904  isstruct2  17074  brssc  17736  isfunc  17786  isfull  17834  isfth  17838  ipole  18455  eqgval  19104  frgpuplem  19699  dvdsr  20296  islindf  21765  ulmval  26343  hpgbr  28781  isausgr  29186  issubgr  29293  isrgr  29582  isrusgr  29584  istrlson  29727  upgrwlkdvspth  29761  ispthson  29764  isspthson  29765  erclwwlkeq  30042  erclwwlkneq  30091  hlimi  31212  isinftm  33212  brfldext  33751  brfinext  33758  finextfldext  33770  bralgext  33803  fldext2chn  33834  constrextdg2lem  33854  metidv  33998  ismntoplly  34131  brae  34347  braew  34348  brfae  34354  satfbrsuc  35509  prv  35571  bj-epelg  37212  bj-ideqgALT  37302  bj-idreseq  37306  bj-idreseqb  37307  bj-ideqg1ALT  37309  brsucmap  38579  brcoss  38633  brcoels  38637  brdmqss  38843  aks6d1c1p1  42300  climf  45810  climf2  45852  nelbr  47462  iscllaw  48377  iscomlaw  48378  isasslaw  48380  islininds  48634  lindepsnlininds  48640