Theorem brab 5393

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 5389	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴𝑅𝐵 ↔ 𝜒))
7	1, 2, 6	mp2an 692	1 ⊢ (𝐴𝑅𝐵 ↔ 𝜒)

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1539   ∈ wcel 2112  Vcvv 3407   class class class wbr 5025  {copab 5087

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 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-ext 2730  ax-sep 5162  ax-nul 5169  ax-pr 5291

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3an 1087  df-tru 1542  df-ex 1783  df-sb 2071  df-clab 2737  df-cleq 2751  df-clel 2831  df-v 3409  df-dif 3857  df-un 3859  df-nul 4222  df-if 4414  df-sn 4516  df-pr 4518  df-op 4522  df-br 5026  df-opab 5088

This theorem is referenced by:  opbrop  5610  f1oweALT  7670  frxp  7818  fnwelem  7823  dftpos4  7914  dfac3  9566  axdc2lem  9893  brdom7disj  9976  brdom6disj  9977  ordpipq  10387  ltresr  10585  shftfn  14465  2shfti  14472  ishpg  26637  brcgr  26778  ex-opab  28301  br8d  30457  br8  33224  br6  33225  br4  33226  xpord2lem  33329  xpord3lem  33335  poseq  33341  dfbigcup2  33735  brsegle  33944  heiborlem2  35515