Theorem brabga 5536

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394   = wceq 1533   ∈ wcel 2098  ⟨cop 4636   class class class wbr 5149  {copab 5211

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696  ax-sep 5300  ax-nul 5307  ax-pr 5429

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-rab 3419  df-v 3463  df-dif 3947  df-un 3949  df-ss 3961  df-nul 4323  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5150  df-opab 5212

This theorem is referenced by:  braba  5539  brabg  5541  epelg  5583  brcog  5869  fmptco  7138  ofrfvalg  7693  isfsupp  9391  wemaplem1  9571  oemapval  9708  wemapwe  9722  fpwwe2lem2  10657  fpwwelem  10670  clim  15474  rlim  15475  vdwmc  16950  isstruct2  17121  brssc  17800  isfunc  17853  isfull  17902  isfth  17906  ipole  18529  eqgval  19140  frgpuplem  19739  dvdsr  20313  islindf  21763  ulmval  26361  hpgbr  28636  isausgr  29049  issubgr  29156  isrgr  29445  isrusgr  29447  istrlson  29593  upgrwlkdvspth  29625  ispthson  29628  isspthson  29629  erclwwlkeq  29900  erclwwlkneq  29949  hlimi  31070  isinftm  32981  brfldext  33470  brfinext  33476  metidv  33624  ismntoplly  33757  brae  33991  braew  33992  brfae  33998  satfbrsuc  35107  prv  35169  bj-epelg  36678  bj-ideqgALT  36768  bj-idreseq  36772  bj-idreseqb  36773  bj-ideqg1ALT  36775  brcoss  38033  brcoels  38037  brdmqss  38248  aks6d1c1p1  41710  climf  45148  climf2  45192  nelbr  46792  iscllaw  47437  iscomlaw  47438  isasslaw  47440  islininds  47700  lindepsnlininds  47706