Theorem brabga 5492

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ⟨cop 4588   class class class wbr 5100  {copab 5162

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5245  ax-pr 5381

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163

This theorem is referenced by:  braba  5495  brabg  5497  epelg  5535  brcog  5825  fmptco  7086  ofrfvalg  7642  isfsupp  9282  wemaplem1  9465  oemapval  9606  wemapwe  9620  fpwwe2lem2  10557  fpwwelem  10570  clim  15431  rlim  15432  vdwmc  16920  isstruct2  17090  brssc  17752  isfunc  17802  isfull  17850  isfth  17854  ipole  18471  eqgval  19123  frgpuplem  19718  dvdsr  20315  islindf  21784  ulmval  26362  hpgbr  28850  isausgr  29255  issubgr  29362  isrgr  29651  isrusgr  29653  istrlson  29796  upgrwlkdvspth  29830  ispthson  29833  isspthson  29834  erclwwlkeq  30111  erclwwlkneq  30160  hlimi  31282  isinftm  33281  brfldext  33829  brfinext  33836  finextfldext  33848  bralgext  33881  fldext2chn  33912  constrextdg2lem  33932  metidv  34076  ismntoplly  34209  brae  34425  braew  34426  brfae  34432  satfbrsuc  35588  prv  35650  bj-epelg  37343  bj-ideqgALT  37440  bj-idreseq  37444  bj-idreseqb  37445  bj-ideqg1ALT  37447  ecqmap  38729  brsucmap  38746  brcoss  38801  brcoels  38805  brdmqss  39010  aks6d1c1p1  42506  climf  46011  climf2  46053  nelbr  47663  iscllaw  48578  iscomlaw  48579  isasslaw  48581  islininds  48835  lindepsnlininds  48841