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 5086	. . 3 ⊢ (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
2		brabga.2	. . . 4 ⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}
3	2	eleq2i 2828	. . 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 1542   ∈ wcel 2114  ⟨cop 4573   class class class wbr 5085  {copab 5147

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-sep 5231  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086  df-opab 5148

This theorem is referenced by:  braba  5492  brabg  5494  epelg  5532  brcog  5821  fmptco  7082  ofrfvalg  7639  isfsupp  9278  wemaplem1  9461  oemapval  9604  wemapwe  9618  fpwwe2lem2  10555  fpwwelem  10568  clim  15456  rlim  15457  vdwmc  16949  isstruct2  17119  brssc  17781  isfunc  17831  isfull  17879  isfth  17883  ipole  18500  eqgval  19152  frgpuplem  19747  dvdsr  20342  islindf  21792  ulmval  26345  hpgbr  28828  isausgr  29233  issubgr  29340  isrgr  29628  isrusgr  29630  istrlson  29773  upgrwlkdvspth  29807  ispthson  29810  isspthson  29811  erclwwlkeq  30088  erclwwlkneq  30137  hlimi  31259  isinftm  33242  brfldext  33789  brfinext  33796  finextfldext  33808  bralgext  33841  fldext2chn  33872  constrextdg2lem  33892  metidv  34036  ismntoplly  34169  brae  34385  braew  34386  brfae  34392  satfbrsuc  35548  prv  35610  bj-epelg  37375  bj-ideqgALT  37472  bj-idreseq  37476  bj-idreseqb  37477  bj-ideqg1ALT  37479  ecqmap  38770  brsucmap  38787  brcoss  38842  brcoels  38846  brdmqss  39051  aks6d1c1p1  42546  climf  46052  climf2  46094  nelbr  47722  iscllaw  48665  iscomlaw  48666  isasslaw  48668  islininds  48922  lindepsnlininds  48928