Theorem opabid 3985

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		vex 2554	. . 3 |- x e. _V
2		vex 2554	. . 3 |- y e. _V
3	1, 2	opex 3957	. 2 |- <.x , y >. e. _V
4		copsexg 3972	. . 3 |- (z = <.x , y >. -> (ph <-> E.xE.y(z = <.x , y >. /\ ph)))
5	4	bicomd 129	. 2 |- (z = <.x , y >. -> (E.xE.y(z = <.x , y >. /\ ph) <-> ph))
6		df-opab 3810	. 2 |- { <.x , y >. | ph } = {z | E.xE.y(z = <.x , y >. /\ ph) }
7	3, 5, 6	elab2 2684	1 |- ( <.x , y >. e. { <.x , y >. | ph } <-> ph)

Syntax hints:   /\ wa 97   <-> wb 98   = wceq 1242  E.wex 1378   e. wcel 1390   <.cop 3370   {copab 3808

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-v 2553  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-opab 3810

This theorem is referenced by:  opelopabsb  3988  ssopab2b  4004  dmopab  4489  rnopab  4524  funopab  4878  funco  4883  fvmptss2  5190  f1ompt  5263  ovid  5559  enssdom  6178