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 5107	. . 3 ⊢ (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
2		brabga.2	. . . 4 ⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}
3	2	eleq2i 2856	. . 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 2147  ⟨cop 4838   class class class wbr 5106  {copab 5170

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5252  ax-pr 5395

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107  df-opab 5171

This theorem is used by:  braba  5515  brabg  5518  epelg  5556  brcog  5849  fmptco  7151  ofrfvalg  7722  isfsupp  9382  wemaplem1  9564  oemapval  9708  wemapwe  9722  fpwwe2lem2  10741  fpwwelem  10754  clim  15687  rlim  15688  vdwmc  17182  isstruct2  17353  brssc  18015  isfunc  18065  isfull  18113  isfth  18117  ipole  18734  eqgval  19415  frgpuplem  20013  dvdsr  20619  islindf  22145  ulmval  26734  hpgbr  29265  isausgr  29772  issubgr  29879  isrgr  30167  isrusgr  30169  istrlson  30316  upgrwlkdvspth  30352  ispthson  30355  isspthson  30356  erclwwlkeq  30636  erclwwlkneq  30685  hlimi  31817  isinftm  33809  brfldext  34344  brfinext  34351  finextfldext  34363  bralgext  34396  fldext2chn  34427  constrextdg2lem  34447  metidv  34591  ismntoplly  34724  brae  34941  braew  34942  brfae  34948  satfbrsuc  36297  prv  36359  bj-epelg  38173  bj-ideqgALT  38270  bj-idreseq  38274  bj-idreseqb  38275  bj-ideqg1ALT  38277  ecqmap  39572  brsucmap  39589  brcoss  39644  brcoels  39648  brdmqss  39853  aks6d1c1p1  43348  climf  46837  climf2  46879  nelbr  48547  iscllaw  49489  iscomlaw  49490  isasslaw  49492  islininds  49761  lindepsnlininds  49767