Theorem opkabssvvk 4208

Description: Any Kuratowski ordered pair abstraction is a subset of (_V X._k _V). (Contributed by SF, 13-Jan-2015.)

Assertion

Ref	Expression
opkabssvvk	|- {x | E.yE.z(x = <<y, z>> /\ ph)} C_ (_V X.k _V)

Distinct variable groups:   x,y   x,z

Allowed substitution hints:   ph(x,y,z)

Proof of Theorem opkabssvvk

Dummy variables w t are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2353	. . . . . . 7 |- <<y, z>> = <<y, z>>
2		vex 2862	. . . . . . . 8 |- y e. _V
3		vex 2862	. . . . . . . 8 |- z e. _V
4		opkeq12 4061	. . . . . . . . 9 |- ((w = y /\ t = z) -> <<w, t>> = <<y, z>>)
5	4	eqeq2d 2364	. . . . . . . 8 |- ((w = y /\ t = z) -> (<<y, z>> = <<w, t>> <-> <<y, z>> = <<y, z>>))
6	2, 3, 5	spc2ev 2947	. . . . . . 7 |- (<<y, z>> = <<y, z>> -> E.wE.t<<y, z>> = <<w, t>>)
7	1, 6	ax-mp 5	. . . . . 6 |- E.wE.t<<y, z>> = <<w, t>>
8		elvvk 4207	. . . . . 6 |- (<<y, z>> e. (_V X.k _V) <-> E.wE.t<<y, z>> = <<w, t>>)
9	7, 8	mpbir 200	. . . . 5 |- <<y, z>> e. (_V X.k _V)
10		eleq1 2413	. . . . 5 |- (x = <<y, z>> -> (x e. (_V X.k _V) <-> <<y, z>> e. (_V X.k _V)))
11	9, 10	mpbiri 224	. . . 4 |- (x = <<y, z>> -> x e. (_V X.k _V))
12	11	adantr 451	. . 3 |- ((x = <<y, z>> /\ ph) -> x e. (_V X.k _V))
13	12	exlimivv 1635	. 2 |- (E.yE.z(x = <<y, z>> /\ ph) -> x e. (_V X.k _V))
14	13	abssi 3341	1 |- {x | E.yE.z(x = <<y, z>> /\ ph)} C_ (_V X.k _V)

Syntax hints:   /\ wa 358  E.wex 1541   = wceq 1642   e. wcel 1710  {cab 2339  _Vcvv 2859   C_ wss 3257  <<copk 4057   X._k cxpk 4174

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4078  ax-sn 4087

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-ne 2518  df-v 2861  df-nin 3211  df-compl 3212  df-in 3213  df-un 3214  df-dif 3215  df-ss 3259  df-nul 3551  df-sn 3741  df-pr 3742  df-opk 4058  df-xpk 4185

This theorem is referenced by:  opkabssvvki  4209