Theorem brabga 5518

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1570   ∈ wcel 2143  ⟨cop 4595   class class class wbr 5109  {copab 5173

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257  ax-pr 5404

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-br 5110  df-opab 5174

This theorem is used by:  braba  5521  brabg  5524  epelg  5562  brcog  5852  fmptco  7125  ofrfvalg  7682  isfsupp  9321  wemaplem1  9504  oemapval  9648  wemapwe  9662  fpwwe2lem2  10621  fpwwelem  10634  clim  15550  rlim  15551  vdwmc  17042  isstruct2  17213  brssc  17875  isfunc  17925  isfull  17973  isfth  17977  ipole  18594  eqgval  19249  frgpuplem  19846  dvdsr  20449  islindf  21971  ulmval  26552  hpgbr  29051  isausgr  29523  issubgr  29630  isrgr  29918  isrusgr  29920  istrlson  30063  upgrwlkdvspth  30097  ispthson  30100  isspthson  30101  erclwwlkeq  30378  erclwwlkneq  30427  hlimi  31549  isinftm  33510  brfldext  34044  brfinext  34051  finextfldext  34063  bralgext  34096  fldext2chn  34127  constrextdg2lem  34147  metidv  34291  ismntoplly  34424  brae  34640  braew  34641  brfae  34647  satfbrsuc  35866  prv  35928  bj-epelg  37732  bj-ideqgALT  37830  bj-idreseq  37834  bj-idreseqb  37835  bj-ideqg1ALT  37837  ecqmap  39126  brsucmap  39143  brcoss  39198  brcoels  39202  brdmqss  39407  aks6d1c1p1  42902  climf  46366  climf2  46408  nelbr  48039  iscllaw  48982  iscomlaw  48983  isasslaw  48985  islininds  49254  lindepsnlininds  49260