Theorem brab 5544

Description: The law of concretion for a binary relation. (Contributed by NM, 16-Aug-1999.)

Hypotheses

Ref	Expression
opelopab.1	⊢ 𝐴 ∈ V
opelopab.2	⊢ 𝐵 ∈ V
opelopab.3	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
opelopab.4	⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))
brab.5	⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}

Assertion

Ref	Expression
brab	⊢ (𝐴𝑅𝐵 ↔ 𝜒)

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

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

Proof of Theorem brab

Step	Hyp	Ref	Expression
1		opelopab.1	. 2 ⊢ 𝐴 ∈ V
2		opelopab.2	. 2 ⊢ 𝐵 ∈ V
3		opelopab.3	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
4		opelopab.4	. . 3 ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))
5		brab.5	. . 3 ⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}
6	3, 4, 5	brabg 5540	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴𝑅𝐵 ↔ 𝜒))
7	1, 2, 6	mp2an 688	1 ⊢ (𝐴𝑅𝐵 ↔ 𝜒)

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539   ∈ wcel 2104  Vcvv 3472   class class class wbr 5149  {copab 5211

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701  ax-sep 5300  ax-nul 5307  ax-pr 5428

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-rab 3431  df-v 3474  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150  df-opab 5212

This theorem is referenced by:  opbrop  5774  f1oweALT  7963  frxp  8116  fnwelem  8121  xpord2lem  8132  xpord3lem  8139  poseq  8148  dftpos4  8234  dfac3  10120  axdc2lem  10447  brdom7disj  10530  brdom6disj  10531  ordpipq  10941  ltresr  11139  shftfn  15026  2shfti  15033  ishpg  28275  brcgr  28423  ex-opab  29950  br8d  32104  br8  35028  br6  35029  br4  35030  dfbigcup2  35173  brsegle  35382  heiborlem2  36985