Theorem brabga 5506

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   = wceq 1562   ∈ wcel 2144  ⟨cop 4590   class class class wbr 5102  {copab 5164

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736  ax-sep 5248  ax-pr 5392

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-rab 3417  df-v 3458  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5103  df-opab 5165

This theorem is referenced by:  braba  5509  brabg  5512  epelg  5550  brcog  5840  fmptco  7113  ofrfvalg  7670  isfsupp  9313  wemaplem1  9496  oemapval  9640  wemapwe  9654  fpwwe2lem2  10592  fpwwelem  10605  clim  15523  rlim  15524  vdwmc  17016  isstruct2  17187  brssc  17849  isfunc  17899  isfull  17947  isfth  17951  ipole  18568  eqgval  19220  frgpuplem  19814  dvdsr  20413  islindf  21866  ulmval  26445  hpgbr  28935  isausgr  29367  issubgr  29474  isrgr  29762  isrusgr  29764  istrlson  29907  upgrwlkdvspth  29941  ispthson  29944  isspthson  29945  erclwwlkeq  30222  erclwwlkneq  30271  hlimi  31393  isinftm  33363  brfldext  33944  brfinext  33951  finextfldext  33963  bralgext  33996  fldext2chn  34027  constrextdg2lem  34047  metidv  34191  ismntoplly  34324  brae  34540  braew  34541  brfae  34547  satfbrsuc  35721  prv  35783  bj-epelg  37558  bj-ideqgALT  37655  bj-idreseq  37659  bj-idreseqb  37660  bj-ideqg1ALT  37662  ecqmap  38953  brsucmap  38970  brcoss  39025  brcoels  39029  brdmqss  39234  aks6d1c1p1  42729  climf  46203  climf2  46245  nelbr  47873  iscllaw  48816  iscomlaw  48817  isasslaw  48819  islininds  49073  lindepsnlininds  49079