Theorem opabid 4707

Description: The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61. (Contributed by NM, 14-Apr-1995.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)

Assertion

Ref	Expression
opabid	|- ( <. x , y >. e. { <. x , y >. | ph } <-> ph )

Proof of Theorem opabid

Dummy variable z is distinct from all other variables.

Step	Hyp	Ref	Expression
1		opex 4663	. 2 |- <. x , y >. e. _V
2		copsexg 4686	. . 3 |- ( z = <. x , y >. -> ( ph <-> E. x E. y ( z = <. x , y >. /\ ph ) ) )
3	2	bicomd 205	. 2 |- ( z = <. x , y >. -> ( E. x E. y ( z = <. x , y >. /\ ph ) <-> ph ) )
4		df-opab 4461	. 2 |- { <. x , y >. | ph } = { z | E. x E. y ( z = <. x , y >. /\ ph ) }
5	1, 3, 4	elab2 3187	1 |- ( <. x , y >. e. { <. x , y >. | ph } <-> ph )

Syntax hints:   <-> wb 188   /\ wa 371   = wceq 1443   E.wex 1662   e. wcel 1886   <.cop 3973   {copab 4459

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-sep 4524  ax-nul 4533  ax-pr 4638

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-eu 2302  df-mo 2303  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-rab 2745  df-v 3046  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-nul 3731  df-if 3881  df-sn 3968  df-pr 3970  df-op 3974  df-opab 4461

This theorem is referenced by:  opelopabsb  4710  ssopab2b  4727  dmopab  5044  rnopab  5078  funopab  5614  opabiota  5926  fvopab5  5972  f1ompt  6042  ovid  6410  zfrep6  6758  enssdom  7591  omxpenlem  7670  infxpenlem  8441  canthwelem  9072  pospo  16212  2ndcdisj  20464  lgsquadlem1  24275  lgsquadlem2  24276  h2hlm  26626  opabdm  28212  opabrn  28213  fpwrelmap  28311  eulerpartlemgvv  29202  phpreu  31922  poimirlem26  31959  diclspsn  34756  areaquad  36095