Theorem brabga 5494

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

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

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 5251  ax-nul 5261  ax-pr 5387

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 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170

This theorem is referenced by:  braba  5497  brabg  5499  epelg  5539  brcog  5830  fmptco  7101  ofrfvalg  7661  isfsupp  9316  wemaplem1  9499  oemapval  9636  wemapwe  9650  fpwwe2lem2  10585  fpwwelem  10598  clim  15460  rlim  15461  vdwmc  16949  isstruct2  17119  brssc  17776  isfunc  17826  isfull  17874  isfth  17878  ipole  18493  eqgval  19109  frgpuplem  19702  dvdsr  20271  islindf  21721  ulmval  26289  hpgbr  28687  isausgr  29091  issubgr  29198  isrgr  29487  isrusgr  29489  istrlson  29635  upgrwlkdvspth  29669  ispthson  29672  isspthson  29673  erclwwlkeq  29947  erclwwlkneq  29996  hlimi  31117  isinftm  33135  brfldext  33641  brfinext  33648  fldext2chn  33718  constrextdg2lem  33738  metidv  33882  ismntoplly  34015  brae  34231  braew  34232  brfae  34238  satfbrsuc  35353  prv  35415  bj-epelg  37056  bj-ideqgALT  37146  bj-idreseq  37150  bj-idreseqb  37151  bj-ideqg1ALT  37153  brcoss  38422  brcoels  38426  brdmqss  38637  aks6d1c1p1  42095  climf  45620  climf2  45664  nelbr  47275  iscllaw  48177  iscomlaw  48178  isasslaw  48180  islininds  48435  lindepsnlininds  48441