Theorem opkabssvvk 4208

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

Assertion

Ref	Expression
opkabssvvk	⊢ {x ∣ ∃y∃z(x = ⟪y, z⟫ ∧ φ)} ⊆ (V ×k V)

Distinct variable groups:   x,y   x,z

Allowed substitution hints:   φ(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 ∈ V
3		vex 2862	. . . . . . . 8 ⊢ z ∈ 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⟫ → ∃w∃t⟪y, z⟫ = ⟪w, t⟫)
7	1, 6	ax-mp 5	. . . . . 6 ⊢ ∃w∃t⟪y, z⟫ = ⟪w, t⟫
8		elvvk 4207	. . . . . 6 ⊢ (⟪y, z⟫ ∈ (V ×k V) ↔ ∃w∃t⟪y, z⟫ = ⟪w, t⟫)
9	7, 8	mpbir 200	. . . . 5 ⊢ ⟪y, z⟫ ∈ (V ×k V)
10		eleq1 2413	. . . . 5 ⊢ (x = ⟪y, z⟫ → (x ∈ (V ×k V) ↔ ⟪y, z⟫ ∈ (V ×k V)))
11	9, 10	mpbiri 224	. . . 4 ⊢ (x = ⟪y, z⟫ → x ∈ (V ×k V))
12	11	adantr 451	. . 3 ⊢ ((x = ⟪y, z⟫ ∧ φ) → x ∈ (V ×k V))
13	12	exlimivv 1635	. 2 ⊢ (∃y∃z(x = ⟪y, z⟫ ∧ φ) → x ∈ (V ×k V))
14	13	abssi 3341	1 ⊢ {x ∣ ∃y∃z(x = ⟪y, z⟫ ∧ φ)} ⊆ (V ×k V)

Syntax hints:   ∧ wa 358  ∃wex 1541   = wceq 1642   ∈ wcel 1710  {cab 2339  Vcvv 2859   ⊆ wss 3257  ⟪copk 4057   ×_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