Theorem brabga 5509

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2108  ⟨cop 4607   class class class wbr 5119  {copab 5181

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 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-br 5120  df-opab 5182

This theorem is referenced by:  braba  5512  brabg  5514  epelg  5554  brcog  5846  fmptco  7118  ofrfvalg  7677  isfsupp  9375  wemaplem1  9558  oemapval  9695  wemapwe  9709  fpwwe2lem2  10644  fpwwelem  10657  clim  15508  rlim  15509  vdwmc  16996  isstruct2  17166  brssc  17825  isfunc  17875  isfull  17923  isfth  17927  ipole  18542  eqgval  19158  frgpuplem  19751  dvdsr  20320  islindf  21770  ulmval  26339  hpgbr  28685  isausgr  29089  issubgr  29196  isrgr  29485  isrusgr  29487  istrlson  29633  upgrwlkdvspth  29667  ispthson  29670  isspthson  29671  erclwwlkeq  29945  erclwwlkneq  29994  hlimi  31115  isinftm  33125  brfldext  33633  brfinext  33640  fldext2chn  33708  constrextdg2lem  33728  metidv  33869  ismntoplly  34002  brae  34218  braew  34219  brfae  34225  satfbrsuc  35334  prv  35396  bj-epelg  37032  bj-ideqgALT  37122  bj-idreseq  37126  bj-idreseqb  37127  bj-ideqg1ALT  37129  brcoss  38395  brcoels  38399  brdmqss  38610  aks6d1c1p1  42066  climf  45599  climf2  45643  nelbr  47251  iscllaw  48112  iscomlaw  48113  isasslaw  48115  islininds  48370  lindepsnlininds  48376