Theorem brabga 5507

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1569   ∈ wcel 2144  ⟨cop 4589   class class class wbr 5102  {copab 5166

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-br 5103  df-opab 5167

This theorem is used by:  braba  5510  brabg  5513  epelg  5551  brcog  5843  fmptco  7130  ofrfvalg  7701  isfsupp  9357  wemaplem1  9540  oemapval  9684  wemapwe  9698  fpwwe2lem2  10717  fpwwelem  10730  clim  15661  rlim  15662  vdwmc  17156  isstruct2  17327  brssc  17989  isfunc  18039  isfull  18087  isfth  18091  ipole  18708  eqgval  19389  frgpuplem  19986  dvdsr  20592  islindf  22118  ulmval  26707  hpgbr  29238  isausgr  29745  issubgr  29852  isrgr  30140  isrusgr  30142  istrlson  30289  upgrwlkdvspth  30325  ispthson  30328  isspthson  30329  erclwwlkeq  30609  erclwwlkneq  30658  hlimi  31790  isinftm  33742  brfldext  34277  brfinext  34284  finextfldext  34296  bralgext  34329  fldext2chn  34360  constrextdg2lem  34380  metidv  34524  ismntoplly  34657  brae  34874  braew  34875  brfae  34881  satfbrsuc  36131  prv  36193  bj-epelg  37983  bj-ideqgALT  38080  bj-idreseq  38084  bj-idreseqb  38085  bj-ideqg1ALT  38087  ecqmap  39382  brsucmap  39399  brcoss  39454  brcoels  39458  brdmqss  39663  aks6d1c1p1  43158  climf  46634  climf2  46676  nelbr  48344  iscllaw  49286  iscomlaw  49287  isasslaw  49289  islininds  49558  lindepsnlininds  49564