Theorem brabg 5497

Description: The law of concretion for a binary relation. (Contributed by NM, 16-Aug-1999.) (Revised by Mario Carneiro, 19-Dec-2013.)

Hypotheses

Ref	Expression
opelopabg.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
opelopabg.2	⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))
brabg.5	⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}

Assertion

Ref	Expression
brabg	⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴𝑅𝐵 ↔ 𝜒))

Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦   𝜒,𝑥,𝑦

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑥,𝑦)   𝐶(𝑥,𝑦)   𝐷(𝑥,𝑦)   𝑅(𝑥,𝑦)

Proof of Theorem brabg

Step	Hyp	Ref	Expression
1		opelopabg.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
2		opelopabg.2	. . 3 ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))
3	1, 2	sylan9bb 509	. 2 ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜒))
4		brabg.5	. 2 ⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}
5	3, 4	brabga 5492	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴𝑅𝐵 ↔ 𝜒))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114   class class class wbr 5100  {copab 5162

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 5245  ax-pr 5381

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163

This theorem is referenced by:  brab  5501  ideqg  5810  brcnvg  5838  f1owe  7311  brrpssg  7682  soseq  8113  breng  8906  brdom2g  8908  brwdom  9486  brttrcl  9636  ltprord  10955  shftfib  15009  efgrelexlema  19695  isref  23470  ltsval  27632  brslts  27775  lrrecval  27952  istrkgld  28548  islnopp  28829  axcontlem5  29059  cmbr  31678  leopg  32216  cvbr  32376  mdbr  32388  dmdbr  32393  isfne  36561  brabg2  37997  isriscg  38264  brssr  38861  lcvbr  39426  bropabg  43709  nthrucw  47273