Theorem brabg 5484

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 5479	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴𝑅𝐵 ↔ 𝜒))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2113   class class class wbr 5095  {copab 5157

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5096  df-opab 5158

This theorem is referenced by:  brab  5488  ideqg  5798  brcnvg  5826  f1owe  7296  brrpssg  7667  soseq  8098  breng  8887  brdom2g  8889  brwdom  9463  brttrcl  9613  ltprord  10931  shftfib  14989  efgrelexlema  19671  isref  23434  sltval  27596  brsslt  27735  lrrecval  27892  istrkgld  28447  islnopp  28727  axcontlem5  28957  cmbr  31575  leopg  32113  cvbr  32273  mdbr  32285  dmdbr  32290  isfne  36394  brabg2  37767  isriscg  38034  brssr  38603  lcvbr  39130  bropabg  43430  nthrucw  46998