Theorem brabga 5480

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ⟨cop 4574   class class class wbr 5086  {copab 5148

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 2709  ax-sep 5231  ax-pr 5368

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 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149

This theorem is referenced by:  braba  5483  brabg  5485  epelg  5523  brcog  5813  fmptco  7074  ofrfvalg  7630  isfsupp  9269  wemaplem1  9452  oemapval  9593  wemapwe  9607  fpwwe2lem2  10544  fpwwelem  10557  clim  15445  rlim  15446  vdwmc  16938  isstruct2  17108  brssc  17770  isfunc  17820  isfull  17868  isfth  17872  ipole  18489  eqgval  19141  frgpuplem  19736  dvdsr  20331  islindf  21800  ulmval  26356  hpgbr  28840  isausgr  29245  issubgr  29352  isrgr  29641  isrusgr  29643  istrlson  29786  upgrwlkdvspth  29820  ispthson  29823  isspthson  29824  erclwwlkeq  30101  erclwwlkneq  30150  hlimi  31272  isinftm  33255  brfldext  33803  brfinext  33810  finextfldext  33822  bralgext  33855  fldext2chn  33886  constrextdg2lem  33906  metidv  34050  ismntoplly  34183  brae  34399  braew  34400  brfae  34406  satfbrsuc  35562  prv  35624  bj-epelg  37381  bj-ideqgALT  37478  bj-idreseq  37482  bj-idreseqb  37483  bj-ideqg1ALT  37485  ecqmap  38774  brsucmap  38791  brcoss  38846  brcoels  38850  brdmqss  39055  aks6d1c1p1  42550  climf  46060  climf2  46102  nelbr  47724  iscllaw  48667  iscomlaw  48668  isasslaw  48670  islininds  48924  lindepsnlininds  48930