New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  sikexlem GIF version

Theorem sikexlem 4295
 Description: Lemma for sikexg 4296. Equality for two subsets of 1c squared . (Contributed by SF, 14-Jan-2015.)
Hypotheses
Ref Expression
sikexlem.1 A (1c ×k 1c)
sikexlem.2 B (1c ×k 1c)
Assertion
Ref Expression
sikexlem (A = Bxy(⟪{x}, {y}⟫ A ↔ ⟪{x}, {y}⟫ B))
Distinct variable groups:   x,A,y   x,B,y

Proof of Theorem sikexlem
Dummy variables z w t are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sikexlem.1 . . 3 A (1c ×k 1c)
2 sikexlem.2 . . 3 B (1c ×k 1c)
3 ssofeq 4077 . . 3 ((A (1c ×k 1c) B (1c ×k 1c)) → (A = Bz (1c ×k 1c)(z Az B)))
41, 2, 3mp2an 653 . 2 (A = Bz (1c ×k 1c)(z Az B))
5 df-ral 2619 . . 3 (z (1c ×k 1c)(z Az B) ↔ z(z (1c ×k 1c) → (z Az B)))
6 elxpk 4196 . . . . . . . 8 (z (1c ×k 1c) ↔ wt(z = ⟪w, t (w 1c t 1c)))
7 el1c 4139 . . . . . . . . . . . . . 14 (w 1cx w = {x})
8 el1c 4139 . . . . . . . . . . . . . 14 (t 1cy t = {y})
97, 8anbi12i 678 . . . . . . . . . . . . 13 ((w 1c t 1c) ↔ (x w = {x} y t = {y}))
10 eeanv 1913 . . . . . . . . . . . . 13 (xy(w = {x} t = {y}) ↔ (x w = {x} y t = {y}))
119, 10bitr4i 243 . . . . . . . . . . . 12 ((w 1c t 1c) ↔ xy(w = {x} t = {y}))
1211anbi2i 675 . . . . . . . . . . 11 ((z = ⟪w, t (w 1c t 1c)) ↔ (z = ⟪w, t xy(w = {x} t = {y})))
13 df-3an 936 . . . . . . . . . . . . . 14 ((w = {x} t = {y} z = ⟪w, t⟫) ↔ ((w = {x} t = {y}) z = ⟪w, t⟫))
14 ancom 437 . . . . . . . . . . . . . 14 (((w = {x} t = {y}) z = ⟪w, t⟫) ↔ (z = ⟪w, t (w = {x} t = {y})))
1513, 14bitri 240 . . . . . . . . . . . . 13 ((w = {x} t = {y} z = ⟪w, t⟫) ↔ (z = ⟪w, t (w = {x} t = {y})))
16152exbii 1583 . . . . . . . . . . . 12 (xy(w = {x} t = {y} z = ⟪w, t⟫) ↔ xy(z = ⟪w, t (w = {x} t = {y})))
17 19.42vv 1907 . . . . . . . . . . . 12 (xy(z = ⟪w, t (w = {x} t = {y})) ↔ (z = ⟪w, t xy(w = {x} t = {y})))
1816, 17bitri 240 . . . . . . . . . . 11 (xy(w = {x} t = {y} z = ⟪w, t⟫) ↔ (z = ⟪w, t xy(w = {x} t = {y})))
1912, 18bitr4i 243 . . . . . . . . . 10 ((z = ⟪w, t (w 1c t 1c)) ↔ xy(w = {x} t = {y} z = ⟪w, t⟫))
20192exbii 1583 . . . . . . . . 9 (wt(z = ⟪w, t (w 1c t 1c)) ↔ wtxy(w = {x} t = {y} z = ⟪w, t⟫))
21 exrot4 1745 . . . . . . . . 9 (xywt(w = {x} t = {y} z = ⟪w, t⟫) ↔ wtxy(w = {x} t = {y} z = ⟪w, t⟫))
2220, 21bitr4i 243 . . . . . . . 8 (wt(z = ⟪w, t (w 1c t 1c)) ↔ xywt(w = {x} t = {y} z = ⟪w, t⟫))
23 snex 4111 . . . . . . . . . 10 {x} V
24 snex 4111 . . . . . . . . . 10 {y} V
25 opkeq1 4059 . . . . . . . . . . 11 (w = {x} → ⟪w, t⟫ = ⟪{x}, t⟫)
2625eqeq2d 2364 . . . . . . . . . 10 (w = {x} → (z = ⟪w, t⟫ ↔ z = ⟪{x}, t⟫))
27 opkeq2 4060 . . . . . . . . . . 11 (t = {y} → ⟪{x}, t⟫ = ⟪{x}, {y}⟫)
2827eqeq2d 2364 . . . . . . . . . 10 (t = {y} → (z = ⟪{x}, t⟫ ↔ z = ⟪{x}, {y}⟫))
2923, 24, 26, 28ceqsex2v 2896 . . . . . . . . 9 (wt(w = {x} t = {y} z = ⟪w, t⟫) ↔ z = ⟪{x}, {y}⟫)
30292exbii 1583 . . . . . . . 8 (xywt(w = {x} t = {y} z = ⟪w, t⟫) ↔ xy z = ⟪{x}, {y}⟫)
316, 22, 303bitri 262 . . . . . . 7 (z (1c ×k 1c) ↔ xy z = ⟪{x}, {y}⟫)
3231imbi1i 315 . . . . . 6 ((z (1c ×k 1c) → (z Az B)) ↔ (xy z = ⟪{x}, {y}⟫ → (z Az B)))
33 19.23vv 1892 . . . . . 6 (xy(z = ⟪{x}, {y}⟫ → (z Az B)) ↔ (xy z = ⟪{x}, {y}⟫ → (z Az B)))
3432, 33bitr4i 243 . . . . 5 ((z (1c ×k 1c) → (z Az B)) ↔ xy(z = ⟪{x}, {y}⟫ → (z Az B)))
3534albii 1566 . . . 4 (z(z (1c ×k 1c) → (z Az B)) ↔ zxy(z = ⟪{x}, {y}⟫ → (z Az B)))
36 alrot3 1738 . . . 4 (zxy(z = ⟪{x}, {y}⟫ → (z Az B)) ↔ xyz(z = ⟪{x}, {y}⟫ → (z Az B)))
3735, 36bitri 240 . . 3 (z(z (1c ×k 1c) → (z Az B)) ↔ xyz(z = ⟪{x}, {y}⟫ → (z Az B)))
38 opkex 4113 . . . . 5 ⟪{x}, {y}⟫ V
39 eleq1 2413 . . . . . 6 (z = ⟪{x}, {y}⟫ → (z A ↔ ⟪{x}, {y}⟫ A))
40 eleq1 2413 . . . . . 6 (z = ⟪{x}, {y}⟫ → (z B ↔ ⟪{x}, {y}⟫ B))
4139, 40bibi12d 312 . . . . 5 (z = ⟪{x}, {y}⟫ → ((z Az B) ↔ (⟪{x}, {y}⟫ A ↔ ⟪{x}, {y}⟫ B)))
4238, 41ceqsalv 2885 . . . 4 (z(z = ⟪{x}, {y}⟫ → (z Az B)) ↔ (⟪{x}, {y}⟫ A ↔ ⟪{x}, {y}⟫ B))
43422albii 1567 . . 3 (xyz(z = ⟪{x}, {y}⟫ → (z Az B)) ↔ xy(⟪{x}, {y}⟫ A ↔ ⟪{x}, {y}⟫ B))
445, 37, 433bitri 262 . 2 (z (1c ×k 1c)(z Az B) ↔ xy(⟪{x}, {y}⟫ A ↔ ⟪{x}, {y}⟫ B))
454, 44bitri 240 1 (A = Bxy(⟪{x}, {y}⟫ A ↔ ⟪{x}, {y}⟫ B))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 176   ∧ wa 358   ∧ w3a 934  ∀wal 1540  ∃wex 1541   = wceq 1642   ∈ wcel 1710  ∀wral 2614   ⊆ wss 3257  {csn 3737  ⟪copk 4057  1cc1c 4134   ×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-3an 936  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-ral 2619  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-1c 4136  df-xpk 4185 This theorem is referenced by:  sikexg  4296
 Copyright terms: Public domain W3C validator