Theorem brabga 4756

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

Syntax hints:   → wi 4   ↔ wb 191   ∧ wa 378   = wceq 1468   ∈ wcel 1937  ⟨cop 4001   class class class wbr 4434  {copab 4492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1698  ax-4 1711  ax-5 1789  ax-6 1836  ax-7 1883  ax-9 1946  ax-10 1965  ax-11 1970  ax-12 1983  ax-13 2137  ax-ext 2485  ax-sep 4558  ax-nul 4567  ax-pr 4680

This theorem depends on definitions:  df-bi 192  df-or 379  df-an 380  df-3an 1023  df-tru 1471  df-ex 1693  df-nf 1697  df-sb 1829  df-eu 2357  df-mo 2358  df-clab 2492  df-cleq 2498  df-clel 2501  df-nfc 2635  df-ne 2677  df-rab 2800  df-v 3068  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-nul 3758  df-if 3909  df-sn 3996  df-pr 3998  df-op 4002  df-br 4435  df-opab 4494

This theorem is referenced by:  braba  4759  brabg  4761  epelg  4792  brcog  5048  fmptco  6124  ofrfval  6615  isfsupp  7972  wemaplem1  8144  oemapval  8273  wemapwe  8287  fpwwe2lem2  9142  fpwwelem  9155  clim  13718  rlim  13719  vdwmc  15090  isstruct2  15291  brssc  15885  isfunc  15935  isfull  15981  isfth  15985  ipole  16569  eqgval  17026  frgpuplem  17583  dvdsr  18034  islindf  19528  ulmval  23496  hpgbr  24963  isuhgra  25186  isushgra  25189  isumgra  25203  isuslgra  25231  isusgra  25232  isausgra  25242  iscusgra  25345  iswlkon  25423  istrlon  25432  ispthon  25467  isspthon  25474  isconngra  25561  isconngra1  25562  erclwwlkeq  25700  erclwwlkneq  25712  iseupa  25853  hlimi  27004  isinftm  28653  metidv  28850  ismntoplly  28984  brae  29218  braew  29219  brfae  29225  climf  38106  isausgr  39794  issubgr  39895  isrgr  40159  isrusgr  40161  istrlson  40314  upgrwlkdvspth  40345  ispthson  40348  isspthson  40349  erclwwlkseq  40639  erclwwlksneq  40651  iscllaw  41015  iscomlaw  41016  isasslaw  41018  islininds  41429  lindepsnlininds  41435