Theorem brabga 5512

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

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

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 2732  ax-sep 5251  ax-pr 5398

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 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168

This theorem is used by:  braba  5515  brabg  5518  epelg  5556  brcog  5848  fmptco  7126  ofrfvalg  7692  isfsupp  9342  wemaplem1  9525  oemapval  9669  wemapwe  9683  fpwwe2lem2  10666  fpwwelem  10679  clim  15606  rlim  15607  vdwmc  17095  isstruct2  17266  brssc  17928  isfunc  17978  isfull  18026  isfth  18030  ipole  18647  eqgval  19328  frgpuplem  19925  dvdsr  20531  islindf  22057  ulmval  26648  hpgbr  29149  isausgr  29656  issubgr  29763  isrgr  30051  isrusgr  30053  istrlson  30200  upgrwlkdvspth  30236  ispthson  30239  isspthson  30240  erclwwlkeq  30520  erclwwlkneq  30569  hlimi  31701  isinftm  33653  brfldext  34188  brfinext  34195  finextfldext  34207  bralgext  34240  fldext2chn  34271  constrextdg2lem  34291  metidv  34435  ismntoplly  34568  brae  34785  braew  34786  brfae  34792  satfbrsuc  36028  prv  36090  bj-epelg  37879  bj-ideqgALT  37975  bj-idreseq  37979  bj-idreseqb  37980  bj-ideqg1ALT  37982  ecqmap  39262  brsucmap  39279  brcoss  39334  brcoels  39338  brdmqss  39543  aks6d1c1p1  43038  climf  46517  climf2  46559  nelbr  48227  iscllaw  49169  iscomlaw  49170  isasslaw  49172  islininds  49441  lindepsnlininds  49447