Theorem brabga 5516

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ⟨cop 4593   class class class wbr 5107  {copab 5171

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-sep 5255  ax-pr 5402

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-br 5108  df-opab 5172

This theorem is used by:  braba  5519  brabg  5522  epelg  5560  brcog  5850  fmptco  7126  ofrfvalg  7689  isfsupp  9338  wemaplem1  9521  oemapval  9665  wemapwe  9679  fpwwe2lem2  10642  fpwwelem  10655  clim  15581  rlim  15582  vdwmc  17072  isstruct2  17243  brssc  17905  isfunc  17955  isfull  18003  isfth  18007  ipole  18624  eqgval  19301  frgpuplem  19898  dvdsr  20502  islindf  22024  ulmval  26611  hpgbr  29113  isausgr  29608  issubgr  29715  isrgr  30003  isrusgr  30005  istrlson  30152  upgrwlkdvspth  30188  ispthson  30191  isspthson  30192  erclwwlkeq  30472  erclwwlkneq  30521  hlimi  31653  isinftm  33606  brfldext  34140  brfinext  34147  finextfldext  34159  bralgext  34192  fldext2chn  34223  constrextdg2lem  34243  metidv  34387  ismntoplly  34520  brae  34737  braew  34738  brfae  34744  satfbrsuc  35930  prv  35992  bj-epelg  37797  bj-ideqgALT  37895  bj-idreseq  37899  bj-idreseqb  37900  bj-ideqg1ALT  37902  ecqmap  39182  brsucmap  39199  brcoss  39254  brcoels  39258  brdmqss  39463  aks6d1c1p1  42958  climf  46437  climf2  46479  nelbr  48147  iscllaw  49089  iscomlaw  49090  isasslaw  49092  islininds  49361  lindepsnlininds  49367