Theorem brabga 5489

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

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

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 5246  ax-nul 5256  ax-pr 5382

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103  df-opab 5165

This theorem is referenced by:  braba  5492  brabg  5494  epelg  5532  brcog  5820  fmptco  7083  ofrfvalg  7641  isfsupp  9292  wemaplem1  9475  oemapval  9612  wemapwe  9626  fpwwe2lem2  10561  fpwwelem  10574  clim  15436  rlim  15437  vdwmc  16925  isstruct2  17095  brssc  17756  isfunc  17806  isfull  17854  isfth  17858  ipole  18475  eqgval  19091  frgpuplem  19686  dvdsr  20282  islindf  21754  ulmval  26322  hpgbr  28740  isausgr  29144  issubgr  29251  isrgr  29540  isrusgr  29542  istrlson  29685  upgrwlkdvspth  29719  ispthson  29722  isspthson  29723  erclwwlkeq  29997  erclwwlkneq  30046  hlimi  31167  isinftm  33150  brfldext  33634  brfinext  33641  fldext2chn  33711  constrextdg2lem  33731  metidv  33875  ismntoplly  34008  brae  34224  braew  34225  brfae  34231  satfbrsuc  35346  prv  35408  bj-epelg  37049  bj-ideqgALT  37139  bj-idreseq  37143  bj-idreseqb  37144  bj-ideqg1ALT  37146  brcoss  38415  brcoels  38419  brdmqss  38630  aks6d1c1p1  42088  climf  45613  climf2  45657  nelbr  47268  iscllaw  48170  iscomlaw  48171  isasslaw  48173  islininds  48428  lindepsnlininds  48434