Theorem brabga 5521

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1567   ∈ wcel 2149  ⟨cop 4600   class class class wbr 5113  {copab 5177

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5261  ax-pr 5407

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5114  df-opab 5178

This theorem is referenced by:  braba  5524  brabg  5527  epelg  5565  brcog  5855  fmptco  7128  ofrfvalg  7685  isfsupp  9327  wemaplem1  9510  oemapval  9654  wemapwe  9668  fpwwe2lem2  10619  fpwwelem  10632  clim  15547  rlim  15548  vdwmc  17040  isstruct2  17211  brssc  17873  isfunc  17923  isfull  17971  isfth  17975  ipole  18592  eqgval  19247  frgpuplem  19844  dvdsr  20446  islindf  21933  ulmval  26511  hpgbr  29003  isausgr  29457  issubgr  29564  isrgr  29852  isrusgr  29854  istrlson  29997  upgrwlkdvspth  30031  ispthson  30034  isspthson  30035  erclwwlkeq  30312  erclwwlkneq  30361  hlimi  31483  isinftm  33444  brfldext  33982  brfinext  33989  finextfldext  34001  bralgext  34034  fldext2chn  34065  constrextdg2lem  34085  metidv  34229  ismntoplly  34362  brae  34578  braew  34579  brfae  34585  satfbrsuc  35793  prv  35855  bj-epelg  37629  bj-ideqgALT  37727  bj-idreseq  37731  bj-idreseqb  37732  bj-ideqg1ALT  37734  ecqmap  39025  brsucmap  39042  brcoss  39097  brcoels  39101  brdmqss  39306  aks6d1c1p1  42801  climf  46267  climf2  46309  nelbr  47937  iscllaw  48880  iscomlaw  48881  isasslaw  48883  islininds  49148  lindepsnlininds  49154