Theorem brabga 5483

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ⟨cop 4587   class class class wbr 5099  {copab 5161

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5242  ax-nul 5252  ax-pr 5378

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3401  df-v 3443  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-br 5100  df-opab 5162

This theorem is referenced by:  braba  5486  brabg  5488  epelg  5526  brcog  5816  fmptco  7076  ofrfvalg  7632  isfsupp  9272  wemaplem1  9455  oemapval  9596  wemapwe  9610  fpwwe2lem2  10547  fpwwelem  10560  clim  15421  rlim  15422  vdwmc  16910  isstruct2  17080  brssc  17742  isfunc  17792  isfull  17840  isfth  17844  ipole  18461  eqgval  19110  frgpuplem  19705  dvdsr  20302  islindf  21771  ulmval  26349  hpgbr  28836  isausgr  29241  issubgr  29348  isrgr  29637  isrusgr  29639  istrlson  29782  upgrwlkdvspth  29816  ispthson  29819  isspthson  29820  erclwwlkeq  30097  erclwwlkneq  30146  hlimi  31267  isinftm  33265  brfldext  33804  brfinext  33811  finextfldext  33823  bralgext  33856  fldext2chn  33887  constrextdg2lem  33907  metidv  34051  ismntoplly  34184  brae  34400  braew  34401  brfae  34407  satfbrsuc  35562  prv  35624  bj-epelg  37271  bj-ideqgALT  37365  bj-idreseq  37369  bj-idreseqb  37370  bj-ideqg1ALT  37372  ecqmap  38652  brsucmap  38669  brcoss  38724  brcoels  38728  brdmqss  38933  aks6d1c1p1  42429  climf  45935  climf2  45977  nelbr  47587  iscllaw  48502  iscomlaw  48503  isasslaw  48505  islininds  48759  lindepsnlininds  48765