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

Theorem oprabid 5550
Description: The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61. (Contributed by Mario Carneiro, 20-Mar-2013.)
Assertion
Ref Expression
oprabid (x, y, z {x, y, z φ} ↔ φ)

Proof of Theorem oprabid
Dummy variables a r s t w are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 vex 2862 . . . 4 x V
2 vex 2862 . . . 4 y V
31, 2opex 4588 . . 3 x, y V
4 vex 2862 . . 3 z V
53, 4opex 4588 . 2 x, y, z V
63, 4eqvinop 4606 . . . . 5 (w = x, y, zat(w = a, t a, t = x, y, z))
76biimpi 186 . . . 4 (w = x, y, zat(w = a, t a, t = x, y, z))
8 eqeq1 2359 . . . . . . . 8 (w = a, t → (w = x, y, za, t = x, y, z))
9 opth 4602 . . . . . . . . 9 (a, t = x, y, z ↔ (a = x, y t = z))
109simplbi 446 . . . . . . . 8 (a, t = x, y, za = x, y)
118, 10syl6bi 219 . . . . . . 7 (w = a, t → (w = x, y, za = x, y))
121, 2eqvinop 4606 . . . . . . . . 9 (a = x, yrs(a = r, s r, s = x, y))
13 opeq1 4578 . . . . . . . . . . . . 13 (a = r, sa, t = r, s, t)
1413eqeq2d 2364 . . . . . . . . . . . 12 (a = r, s → (w = a, tw = r, s, t))
15 opth 4602 . . . . . . . . . . . . . . . . . . 19 (x, y, z = r, s, t ↔ (x, y = r, s z = t))
16 opth 4602 . . . . . . . . . . . . . . . . . . . 20 (x, y = r, s ↔ (x = r y = s))
1716anbi1i 676 . . . . . . . . . . . . . . . . . . 19 ((x, y = r, s z = t) ↔ ((x = r y = s) z = t))
1815, 17bitri 240 . . . . . . . . . . . . . . . . . 18 (x, y, z = r, s, t ↔ ((x = r y = s) z = t))
1918anbi1i 676 . . . . . . . . . . . . . . . . 17 ((x, y, z = r, s, t φ) ↔ (((x = r y = s) z = t) φ))
20 anass 630 . . . . . . . . . . . . . . . . 17 ((((x = r y = s) z = t) φ) ↔ ((x = r y = s) (z = t φ)))
21 anass 630 . . . . . . . . . . . . . . . . 17 (((x = r y = s) (z = t φ)) ↔ (x = r (y = s (z = t φ))))
2219, 20, 213bitri 262 . . . . . . . . . . . . . . . 16 ((x, y, z = r, s, t φ) ↔ (x = r (y = s (z = t φ))))
23223exbii 1584 . . . . . . . . . . . . . . 15 (xyz(x, y, z = r, s, t φ) ↔ xyz(x = r (y = s (z = t φ))))
24 nfcvf2 2512 . . . . . . . . . . . . . . . . . . . 20 x x = zzx)
25 nfcvd 2490 . . . . . . . . . . . . . . . . . . . 20 x x = zzr)
2624, 25nfeqd 2503 . . . . . . . . . . . . . . . . . . 19 x x = z → Ⅎz x = r)
2726exdistrf 1971 . . . . . . . . . . . . . . . . . 18 (xz(x = r (y = s (z = t φ))) → x(x = r z(y = s (z = t φ))))
2827eximi 1576 . . . . . . . . . . . . . . . . 17 (yxz(x = r (y = s (z = t φ))) → yx(x = r z(y = s (z = t φ))))
29 excom 1741 . . . . . . . . . . . . . . . . 17 (xyz(x = r (y = s (z = t φ))) ↔ yxz(x = r (y = s (z = t φ))))
30 excom 1741 . . . . . . . . . . . . . . . . 17 (xy(x = r z(y = s (z = t φ))) ↔ yx(x = r z(y = s (z = t φ))))
3128, 29, 303imtr4i 257 . . . . . . . . . . . . . . . 16 (xyz(x = r (y = s (z = t φ))) → xy(x = r z(y = s (z = t φ))))
32 nfcvf2 2512 . . . . . . . . . . . . . . . . . 18 x x = yyx)
33 nfcvd 2490 . . . . . . . . . . . . . . . . . 18 x x = yyr)
3432, 33nfeqd 2503 . . . . . . . . . . . . . . . . 17 x x = y → Ⅎy x = r)
3534exdistrf 1971 . . . . . . . . . . . . . . . 16 (xy(x = r z(y = s (z = t φ))) → x(x = r yz(y = s (z = t φ))))
36 nfcvf2 2512 . . . . . . . . . . . . . . . . . . . 20 y y = zzy)
37 nfcvd 2490 . . . . . . . . . . . . . . . . . . . 20 y y = zzs)
3836, 37nfeqd 2503 . . . . . . . . . . . . . . . . . . 19 y y = z → Ⅎz y = s)
3938exdistrf 1971 . . . . . . . . . . . . . . . . . 18 (yz(y = s (z = t φ)) → y(y = s z(z = t φ)))
4039anim2i 552 . . . . . . . . . . . . . . . . 17 ((x = r yz(y = s (z = t φ))) → (x = r y(y = s z(z = t φ))))
4140eximi 1576 . . . . . . . . . . . . . . . 16 (x(x = r yz(y = s (z = t φ))) → x(x = r y(y = s z(z = t φ))))
4231, 35, 413syl 18 . . . . . . . . . . . . . . 15 (xyz(x = r (y = s (z = t φ))) → x(x = r y(y = s z(z = t φ))))
4323, 42sylbi 187 . . . . . . . . . . . . . 14 (xyz(x, y, z = r, s, t φ) → x(x = r y(y = s z(z = t φ))))
44 df-3an 936 . . . . . . . . . . . . . . . . 17 ((x = r y = s z = t) ↔ ((x = r y = s) z = t))
4518, 44bitr4i 243 . . . . . . . . . . . . . . . 16 (x, y, z = r, s, t ↔ (x = r y = s z = t))
46 euequ1 2292 . . . . . . . . . . . . . . . . . . 19 ∃!x x = r
47 eupick 2267 . . . . . . . . . . . . . . . . . . 19 ((∃!x x = r x(x = r y(y = s z(z = t φ)))) → (x = ry(y = s z(z = t φ))))
4846, 47mpan 651 . . . . . . . . . . . . . . . . . 18 (x(x = r y(y = s z(z = t φ))) → (x = ry(y = s z(z = t φ))))
49 euequ1 2292 . . . . . . . . . . . . . . . . . . . 20 ∃!y y = s
50 eupick 2267 . . . . . . . . . . . . . . . . . . . 20 ((∃!y y = s y(y = s z(z = t φ))) → (y = sz(z = t φ)))
5149, 50mpan 651 . . . . . . . . . . . . . . . . . . 19 (y(y = s z(z = t φ)) → (y = sz(z = t φ)))
52 euequ1 2292 . . . . . . . . . . . . . . . . . . . 20 ∃!z z = t
53 eupick 2267 . . . . . . . . . . . . . . . . . . . 20 ((∃!z z = t z(z = t φ)) → (z = tφ))
5452, 53mpan 651 . . . . . . . . . . . . . . . . . . 19 (z(z = t φ) → (z = tφ))
5551, 54syl6 29 . . . . . . . . . . . . . . . . . 18 (y(y = s z(z = t φ)) → (y = s → (z = tφ)))
5648, 55syl6 29 . . . . . . . . . . . . . . . . 17 (x(x = r y(y = s z(z = t φ))) → (x = r → (y = s → (z = tφ))))
57563impd 1165 . . . . . . . . . . . . . . . 16 (x(x = r y(y = s z(z = t φ))) → ((x = r y = s z = t) → φ))
5845, 57syl5bi 208 . . . . . . . . . . . . . . 15 (x(x = r y(y = s z(z = t φ))) → (x, y, z = r, s, tφ))
5958com12 27 . . . . . . . . . . . . . 14 (x, y, z = r, s, t → (x(x = r y(y = s z(z = t φ))) → φ))
6043, 59syl5 28 . . . . . . . . . . . . 13 (x, y, z = r, s, t → (xyz(x, y, z = r, s, t φ) → φ))
61 eqeq1 2359 . . . . . . . . . . . . . . 15 (w = r, s, t → (w = x, y, zr, s, t = x, y, z))
62 eqcom 2355 . . . . . . . . . . . . . . 15 (r, s, t = x, y, zx, y, z = r, s, t)
6361, 62syl6bb 252 . . . . . . . . . . . . . 14 (w = r, s, t → (w = x, y, zx, y, z = r, s, t))
6463anbi1d 685 . . . . . . . . . . . . . . . 16 (w = r, s, t → ((w = x, y, z φ) ↔ (x, y, z = r, s, t φ)))
65643exbidv 1629 . . . . . . . . . . . . . . 15 (w = r, s, t → (xyz(w = x, y, z φ) ↔ xyz(x, y, z = r, s, t φ)))
6665imbi1d 308 . . . . . . . . . . . . . 14 (w = r, s, t → ((xyz(w = x, y, z φ) → φ) ↔ (xyz(x, y, z = r, s, t φ) → φ)))
6763, 66imbi12d 311 . . . . . . . . . . . . 13 (w = r, s, t → ((w = x, y, z → (xyz(w = x, y, z φ) → φ)) ↔ (x, y, z = r, s, t → (xyz(x, y, z = r, s, t φ) → φ))))
6860, 67mpbiri 224 . . . . . . . . . . . 12 (w = r, s, t → (w = x, y, z → (xyz(w = x, y, z φ) → φ)))
6914, 68syl6bi 219 . . . . . . . . . . 11 (a = r, s → (w = a, t → (w = x, y, z → (xyz(w = x, y, z φ) → φ))))
7069adantr 451 . . . . . . . . . 10 ((a = r, s r, s = x, y) → (w = a, t → (w = x, y, z → (xyz(w = x, y, z φ) → φ))))
7170exlimivv 1635 . . . . . . . . 9 (rs(a = r, s r, s = x, y) → (w = a, t → (w = x, y, z → (xyz(w = x, y, z φ) → φ))))
7212, 71sylbi 187 . . . . . . . 8 (a = x, y → (w = a, t → (w = x, y, z → (xyz(w = x, y, z φ) → φ))))
7372com3l 75 . . . . . . 7 (w = a, t → (w = x, y, z → (a = x, y → (xyz(w = x, y, z φ) → φ))))
7411, 73mpdd 36 . . . . . 6 (w = a, t → (w = x, y, z → (xyz(w = x, y, z φ) → φ)))
7574adantr 451 . . . . 5 ((w = a, t a, t = x, y, z) → (w = x, y, z → (xyz(w = x, y, z φ) → φ)))
7675exlimivv 1635 . . . 4 (at(w = a, t a, t = x, y, z) → (w = x, y, z → (xyz(w = x, y, z φ) → φ)))
777, 76mpcom 32 . . 3 (w = x, y, z → (xyz(w = x, y, z φ) → φ))
78 19.8a 1756 . . . . 5 ((w = x, y, z φ) → z(w = x, y, z φ))
79 19.8a 1756 . . . . 5 (z(w = x, y, z φ) → yz(w = x, y, z φ))
80 19.8a 1756 . . . . 5 (yz(w = x, y, z φ) → xyz(w = x, y, z φ))
8178, 79, 803syl 18 . . . 4 ((w = x, y, z φ) → xyz(w = x, y, z φ))
8281ex 423 . . 3 (w = x, y, z → (φxyz(w = x, y, z φ)))
8377, 82impbid 183 . 2 (w = x, y, z → (xyz(w = x, y, z φ) ↔ φ))
84 df-oprab 5528 . 2 {x, y, z φ} = {w xyz(w = x, y, z φ)}
855, 83, 84elab2 2988 1 (x, y, z {x, y, z φ} ↔ φ)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 176   wa 358   w3a 934  wal 1540  wex 1541   = wceq 1642   wcel 1710  ∃!weu 2204  cop 4561  {coprab 5527
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-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4078  ax-xp 4079  ax-cnv 4080  ax-1c 4081  ax-sset 4082  ax-si 4083  ax-ins2 4084  ax-ins3 4085  ax-typlower 4086  ax-sn 4087
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2208  df-mo 2209  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-ne 2518  df-ral 2619  df-rex 2620  df-reu 2621  df-rmo 2622  df-rab 2623  df-v 2861  df-sbc 3047  df-nin 3211  df-compl 3212  df-in 3213  df-un 3214  df-dif 3215  df-symdif 3216  df-ss 3259  df-pss 3261  df-nul 3551  df-if 3663  df-pw 3724  df-sn 3741  df-pr 3742  df-uni 3892  df-int 3927  df-opk 4058  df-1c 4136  df-pw1 4137  df-uni1 4138  df-xpk 4185  df-cnvk 4186  df-ins2k 4187  df-ins3k 4188  df-imak 4189  df-cok 4190  df-p6 4191  df-sik 4192  df-ssetk 4193  df-imagek 4194  df-idk 4195  df-iota 4339  df-0c 4377  df-addc 4378  df-nnc 4379  df-fin 4380  df-lefin 4440  df-ltfin 4441  df-ncfin 4442  df-tfin 4443  df-evenfin 4444  df-oddfin 4445  df-sfin 4446  df-spfin 4447  df-phi 4565  df-op 4566  df-proj1 4567  df-proj2 4568  df-oprab 5528
This theorem is referenced by:  ovidig  5593
  Copyright terms: Public domain W3C validator