Theorem brabg 5539

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 511	. 2 ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜒))
4		brabg.5	. 2 ⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}
5	3, 4	brabga 5534	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴𝑅𝐵 ↔ 𝜒))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107   class class class wbr 5148  {copab 5210

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5299  ax-nul 5306  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149  df-opab 5211

This theorem is referenced by:  brab  5543  ideqg  5850  brcnvg  5878  f1owe  7347  brrpssg  7712  soseq  8142  breng  8945  brenOLD  8947  brdom2g  8948  brdomgOLD  8950  brwdom  9559  brttrcl  9705  ltprord  11022  shftfib  15016  efgrelexlema  19612  isref  23005  sltval  27140  brsslt  27277  lrrecval  27413  istrkgld  27700  islnopp  27980  axcontlem5  28216  cmbr  30825  leopg  31363  cvbr  31523  mdbr  31535  dmdbr  31540  isfne  35213  brabg2  36574  isriscg  36841  brssr  37360  lcvbr  37880  bropabg  42059