Theorem brabga 5423

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1537   ∈ wcel 2114  ⟨cop 4575   class class class wbr 5068  {copab 5130

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pr 5332

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-br 5069  df-opab 5131

This theorem is referenced by:  braba  5426  brabg  5428  epelg  5468  epelgOLD  5469  brcog  5739  fmptco  6893  ofrfval  7419  isfsupp  8839  wemaplem1  9012  oemapval  9148  wemapwe  9162  fpwwe2lem2  10056  fpwwelem  10069  clim  14853  rlim  14854  vdwmc  16316  isstruct2  16495  brssc  17086  isfunc  17136  isfull  17182  isfth  17186  ipole  17770  eqgval  18331  frgpuplem  18900  dvdsr  19398  islindf  20958  ulmval  24970  hpgbr  26548  isausgr  26951  issubgr  27055  isrgr  27343  isrusgr  27345  istrlson  27490  upgrwlkdvspth  27522  ispthson  27525  isspthson  27526  erclwwlkeq  27798  erclwwlkneq  27848  hlimi  28967  isinftm  30812  brfldext  31039  brfinext  31045  metidv  31134  ismntoplly  31268  brae  31502  braew  31503  brfae  31509  satfbrsuc  32615  prv  32677  bj-epelg  34362  bj-ideqgALT  34452  bj-idreseq  34456  bj-idreseqb  34457  bj-ideqg1ALT  34459  brcoss  35678  brcoels  35682  brdmqss  35883  climf  41910  climf2  41954  nelbr  43480  isomgr  43995  iscllaw  44103  iscomlaw  44104  isasslaw  44106  islininds  44508  lindepsnlininds  44514