Theorem brab 3732

Description: The law of concretion for a binary relation.

Hypotheses

Ref	Expression
opelopab.1	|- A e. _V
opelopab.2	|- B e. _V
opelopab.3	|- (x = A -> (ph <-> ps))
opelopab.4	|- (y = B -> (ps <-> ch))
brab.5	|- R = {<.x, y>. | ph}

Assertion

Ref	Expression
brab	|- (ARB <-> ch)

Distinct variable groups:   x,y,A   x,B,y   ch,x,y

Proof of Theorem brab

Step	Hyp	Ref	Expression
1		opelopab.1	. 2 |- A e. _V
2		opelopab.2	. 2 |- B e. _V
3		opelopab.3	. . 3 |- (x = A -> (ph <-> ps))
4		opelopab.4	. . 3 |- (y = B -> (ps <-> ch))
5		brab.5	. . 3 |- R = {<.x, y>. | ph}
6	3, 4, 5	brabg 3729	. 2 |- ((A e. _V /\ B e. _V) -> (ARB <-> ch))
7	1, 2, 6	mp2an 681	1 |- (ARB <-> ch)

Syntax hints:   -> wi 3   <-> wb 219   = wceq 1586   e. wcel 1588  _Vcvv 2538   class class class wbr 3507  {copab 3565

This theorem is referenced by:  epelc 3745  opbrop 4197  opelco 4259  f1oweALT 4980  frxp 5210  fnwelem 5215  aceq3 6187  axdc2lem 6303  zornlem 6368  brdom7disj 6380  brdom6disj 6381  ltresr 6776  hlimi 11525  frxpOLD 14604  poseq 14607  dfbigcup2 14760  inposetlem 15357  hartoglem 16207  filnetlem3 16466  filnetlem4 16467  filnetlem5 16468  filnet 16469

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1592  ax-gen 1593  ax-8 1594  ax-9 1595  ax-10 1596  ax-11 1597  ax-12 1598  ax-14 1600  ax-17 1605  ax-4 1608  ax-5o 1610  ax-6o 1613  ax-9o 1763  ax-10o 1781  ax-16 1854  ax-11o 1864  ax-ext 2123  ax-sep 3606  ax-nul 3613  ax-pow 3649  ax-pr 3687

This theorem depends on definitions:  df-bi 220  df-or 338  df-an 339  df-ex 1616  df-sb 1816  df-eu 2041  df-mo 2042  df-clab 2129  df-cleq 2134  df-clel 2137  df-ne 2268  df-v 2540  df-dif 2830  df-un 2832  df-in 2834  df-ss 2836  df-nul 3083  df-pw 3229  df-sn 3242  df-pr 3243  df-op 3246  df-br 3508  df-opab 3566

Copyright terms: Public domain