Theorem brabga 5390

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1542   ∈ wcel 2114  ⟨cop 4523   class class class wbr 5031  {copab 5093

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2711  ax-sep 5168  ax-nul 5175  ax-pr 5297

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2075  df-clab 2718  df-cleq 2731  df-clel 2812  df-v 3401  df-dif 3847  df-un 3849  df-nul 4213  df-if 4416  df-sn 4518  df-pr 4520  df-op 4524  df-br 5032  df-opab 5094

This theorem is referenced by:  braba  5393  brabg  5395  epelg  5436  brcog  5710  fmptco  6904  ofrfvalg  7435  isfsupp  8913  wemaplem1  9086  oemapval  9222  wemapwe  9236  fpwwe2lem2  10135  fpwwelem  10148  clim  14944  rlim  14945  vdwmc  16417  isstruct2  16599  brssc  17192  isfunc  17242  isfull  17288  isfth  17292  ipole  17887  eqgval  18450  frgpuplem  19019  dvdsr  19521  islindf  20631  ulmval  25130  hpgbr  26709  isausgr  27112  issubgr  27216  isrgr  27504  isrusgr  27506  istrlson  27651  upgrwlkdvspth  27683  ispthson  27686  isspthson  27687  erclwwlkeq  27958  erclwwlkneq  28007  hlimi  29126  isinftm  31015  brfldext  31297  brfinext  31303  metidv  31417  ismntoplly  31548  brae  31782  braew  31783  brfae  31789  satfbrsuc  32902  prv  32964  bj-epelg  34884  bj-ideqgALT  34973  bj-idreseq  34977  bj-idreseqb  34978  bj-ideqg1ALT  34980  brcoss  36200  brcoels  36204  brdmqss  36405  climf  42728  climf2  42772  nelbr  44329  isomgr  44839  iscllaw  44947  iscomlaw  44948  isasslaw  44950  islininds  45351  lindepsnlininds  45357