Theorem brabga 5477

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ⟨cop 4583   class class class wbr 5092  {copab 5154

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371

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 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5093  df-opab 5155

This theorem is referenced by:  braba  5480  brabg  5482  epelg  5520  brcog  5809  fmptco  7063  ofrfvalg  7621  isfsupp  9255  wemaplem1  9438  oemapval  9579  wemapwe  9593  fpwwe2lem2  10526  fpwwelem  10539  clim  15401  rlim  15402  vdwmc  16890  isstruct2  17060  brssc  17721  isfunc  17771  isfull  17819  isfth  17823  ipole  18440  eqgval  19056  frgpuplem  19651  dvdsr  20247  islindf  21719  ulmval  26287  hpgbr  28705  isausgr  29109  issubgr  29216  isrgr  29505  isrusgr  29507  istrlson  29650  upgrwlkdvspth  29684  ispthson  29687  isspthson  29688  erclwwlkeq  29962  erclwwlkneq  30011  hlimi  31132  isinftm  33124  brfldext  33618  brfinext  33625  finextfldext  33637  bralgext  33670  fldext2chn  33701  constrextdg2lem  33721  metidv  33865  ismntoplly  33998  brae  34214  braew  34215  brfae  34221  satfbrsuc  35349  prv  35411  bj-epelg  37052  bj-ideqgALT  37142  bj-idreseq  37146  bj-idreseqb  37147  bj-ideqg1ALT  37149  brcoss  38418  brcoels  38422  brdmqss  38633  aks6d1c1p1  42090  climf  45613  climf2  45657  nelbr  47268  iscllaw  48183  iscomlaw  48184  isasslaw  48186  islininds  48441  lindepsnlininds  48447