Theorem opabid 4696

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 4654	. 2 |- <. x , y >. e. _V
2		copsexg 4675	. . 3 |- ( z = <. x , y >. -> ( ph <-> E. x E. y ( z = <. x , y >. /\ ph ) ) )
3	2	bicomd 201	. 2 |- ( z = <. x , y >. -> ( E. x E. y ( z = <. x , y >. /\ ph ) <-> ph ) )
4		df-opab 4453	. 2 |- { <. x , y >. | ph } = { z | E. x E. y ( z = <. x , y >. /\ ph ) }
5	1, 3, 4	elab2 3198	1 |- ( <. x , y >. e. { <. x , y >. | ph } <-> ph )

Syntax hints:   <-> wb 184   /\ wa 367   = wceq 1405   E.wex 1633   e. wcel 1842   <.cop 3977   {copab 4451

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-sep 4516  ax-nul 4524  ax-pr 4629

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-rab 2762  df-v 3060  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-nul 3738  df-if 3885  df-sn 3972  df-pr 3974  df-op 3978  df-opab 4453

This theorem is referenced by:  opelopabsb  4699  ssopab2b  4716  dmopab  5033  rnopab  5067  funopab  5601  opabiota  5911  fvopab5  5956  f1ompt  6030  ovid  6399  zfrep6  6751  enssdom  7577  omxpenlem  7655  infxpenlem  8422  canthwelem  9057  pospo  15925  2ndcdisj  20247  lgsquadlem1  24008  lgsquadlem2  24009  h2hlm  26297  opabdm  27887  opabrn  27888  fpwrelmap  27989  eulerpartlemgvv  28807  diclspsn  34194  areaquad  35528