Theorem brabga 5535

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394   = wceq 1539   ∈ wcel 2104  ⟨cop 4635   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 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701  ax-sep 5300  ax-nul 5307  ax-pr 5428

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-rab 3431  df-v 3474  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150  df-opab 5212

This theorem is referenced by:  braba  5538  brabg  5540  epelg  5582  brcog  5867  fmptco  7130  ofrfvalg  7682  isfsupp  9369  wemaplem1  9545  oemapval  9682  wemapwe  9696  fpwwe2lem2  10631  fpwwelem  10644  clim  15444  rlim  15445  vdwmc  16917  isstruct2  17088  brssc  17767  isfunc  17820  isfull  17867  isfth  17871  ipole  18493  eqgval  19095  frgpuplem  19683  dvdsr  20255  islindf  21588  ulmval  26126  hpgbr  28276  isausgr  28689  issubgr  28793  isrgr  29081  isrusgr  29083  istrlson  29229  upgrwlkdvspth  29261  ispthson  29264  isspthson  29265  erclwwlkeq  29536  erclwwlkneq  29585  hlimi  30706  isinftm  32595  brfldext  33012  brfinext  33018  metidv  33168  ismntoplly  33301  brae  33535  braew  33536  brfae  33542  satfbrsuc  34653  prv  34715  bj-epelg  36254  bj-ideqgALT  36344  bj-idreseq  36348  bj-idreseqb  36349  bj-ideqg1ALT  36351  brcoss  37606  brcoels  37610  brdmqss  37821  climf  44638  climf2  44682  nelbr  46282  isomgr  46791  iscllaw  46867  iscomlaw  46868  isasslaw  46870  islininds  47216  lindepsnlininds  47222