Theorem brabga 5484

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 5483	. 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 5232  ax-pr 5372

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  5487  brabg  5489  epelg  5527  brcog  5817  fmptco  7078  ofrfvalg  7634  isfsupp  9273  wemaplem1  9456  oemapval  9599  wemapwe  9613  fpwwe2lem2  10550  fpwwelem  10563  clim  15451  rlim  15452  vdwmc  16944  isstruct2  17114  brssc  17776  isfunc  17826  isfull  17874  isfth  17878  ipole  18495  eqgval  19147  frgpuplem  19742  dvdsr  20337  islindf  21806  ulmval  26362  hpgbr  28846  isausgr  29251  issubgr  29358  isrgr  29647  isrusgr  29649  istrlson  29792  upgrwlkdvspth  29826  ispthson  29829  isspthson  29830  erclwwlkeq  30107  erclwwlkneq  30156  hlimi  31278  isinftm  33261  brfldext  33809  brfinext  33816  finextfldext  33828  bralgext  33861  fldext2chn  33892  constrextdg2lem  33912  metidv  34056  ismntoplly  34189  brae  34405  braew  34406  brfae  34412  satfbrsuc  35568  prv  35630  bj-epelg  37395  bj-ideqgALT  37492  bj-idreseq  37496  bj-idreseqb  37497  bj-ideqg1ALT  37499  ecqmap  38788  brsucmap  38805  brcoss  38860  brcoels  38864  brdmqss  39069  aks6d1c1p1  42564  climf  46074  climf2  46116  nelbr  47738  iscllaw  48681  iscomlaw  48682  isasslaw  48684  islininds  48938  lindepsnlininds  48944