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

Theorem 2mo 2282
 Description: Two equivalent expressions for double "at most one." (Contributed by NM, 2-Feb-2005.) (Revised by Mario Carneiro, 17-Oct-2016.)
Assertion
Ref Expression
2mo (zwxy(φ → (x = z y = w)) ↔ xyzw((φ [z / x][w / y]φ) → (x = z y = w)))
Distinct variable groups:   x,y,z,w   φ,z,w
Allowed substitution hints:   φ(x,y)

Proof of Theorem 2mo
Dummy variables v u are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 equequ2 1686 . . . . . . 7 (v = z → (x = vx = z))
2 equequ2 1686 . . . . . . 7 (u = w → (y = uy = w))
31, 2bi2anan9 843 . . . . . 6 ((v = z u = w) → ((x = v y = u) ↔ (x = z y = w)))
43imbi2d 307 . . . . 5 ((v = z u = w) → ((φ → (x = v y = u)) ↔ (φ → (x = z y = w))))
542albidv 1627 . . . 4 ((v = z u = w) → (xy(φ → (x = v y = u)) ↔ xy(φ → (x = z y = w))))
65cbvex2v 2007 . . 3 (vuxy(φ → (x = v y = u)) ↔ zwxy(φ → (x = z y = w)))
7 nfv 1619 . . . . . . . . 9 z(φ → (x = v y = u))
8 nfv 1619 . . . . . . . . 9 w(φ → (x = v y = u))
9 nfs1v 2106 . . . . . . . . . 10 x[z / x][w / y]φ
10 nfv 1619 . . . . . . . . . 10 x(z = v w = u)
119, 10nfim 1813 . . . . . . . . 9 x([z / x][w / y]φ → (z = v w = u))
12 nfs1v 2106 . . . . . . . . . . 11 y[w / y]φ
1312nfsb 2109 . . . . . . . . . 10 y[z / x][w / y]φ
14 nfv 1619 . . . . . . . . . 10 y(z = v w = u)
1513, 14nfim 1813 . . . . . . . . 9 y([z / x][w / y]φ → (z = v w = u))
16 sbequ12 1919 . . . . . . . . . . 11 (y = w → (φ ↔ [w / y]φ))
17 sbequ12 1919 . . . . . . . . . . 11 (x = z → ([w / y]φ ↔ [z / x][w / y]φ))
1816, 17sylan9bbr 681 . . . . . . . . . 10 ((x = z y = w) → (φ ↔ [z / x][w / y]φ))
19 equequ1 1684 . . . . . . . . . . 11 (x = z → (x = vz = v))
20 equequ1 1684 . . . . . . . . . . 11 (y = w → (y = uw = u))
2119, 20bi2anan9 843 . . . . . . . . . 10 ((x = z y = w) → ((x = v y = u) ↔ (z = v w = u)))
2218, 21imbi12d 311 . . . . . . . . 9 ((x = z y = w) → ((φ → (x = v y = u)) ↔ ([z / x][w / y]φ → (z = v w = u))))
237, 8, 11, 15, 22cbval2 2004 . . . . . . . 8 (xy(φ → (x = v y = u)) ↔ zw([z / x][w / y]φ → (z = v w = u)))
2423biimpi 186 . . . . . . 7 (xy(φ → (x = v y = u)) → zw([z / x][w / y]φ → (z = v w = u)))
2524ancli 534 . . . . . 6 (xy(φ → (x = v y = u)) → (xy(φ → (x = v y = u)) zw([z / x][w / y]φ → (z = v w = u))))
26 alcom 1737 . . . . . . . . 9 (yzw((φ → (x = v y = u)) ([z / x][w / y]φ → (z = v w = u))) ↔ zyw((φ → (x = v y = u)) ([z / x][w / y]φ → (z = v w = u))))
278, 15aaan 1884 . . . . . . . . . 10 (yw((φ → (x = v y = u)) ([z / x][w / y]φ → (z = v w = u))) ↔ (y(φ → (x = v y = u)) w([z / x][w / y]φ → (z = v w = u))))
2827albii 1566 . . . . . . . . 9 (zyw((φ → (x = v y = u)) ([z / x][w / y]φ → (z = v w = u))) ↔ z(y(φ → (x = v y = u)) w([z / x][w / y]φ → (z = v w = u))))
2926, 28bitri 240 . . . . . . . 8 (yzw((φ → (x = v y = u)) ([z / x][w / y]φ → (z = v w = u))) ↔ z(y(φ → (x = v y = u)) w([z / x][w / y]φ → (z = v w = u))))
3029albii 1566 . . . . . . 7 (xyzw((φ → (x = v y = u)) ([z / x][w / y]φ → (z = v w = u))) ↔ xz(y(φ → (x = v y = u)) w([z / x][w / y]φ → (z = v w = u))))
31 nfv 1619 . . . . . . . 8 zy(φ → (x = v y = u))
3211nfal 1842 . . . . . . . 8 xw([z / x][w / y]φ → (z = v w = u))
3331, 32aaan 1884 . . . . . . 7 (xz(y(φ → (x = v y = u)) w([z / x][w / y]φ → (z = v w = u))) ↔ (xy(φ → (x = v y = u)) zw([z / x][w / y]φ → (z = v w = u))))
3430, 33bitri 240 . . . . . 6 (xyzw((φ → (x = v y = u)) ([z / x][w / y]φ → (z = v w = u))) ↔ (xy(φ → (x = v y = u)) zw([z / x][w / y]φ → (z = v w = u))))
3525, 34sylibr 203 . . . . 5 (xy(φ → (x = v y = u)) → xyzw((φ → (x = v y = u)) ([z / x][w / y]φ → (z = v w = u))))
36 prth 554 . . . . . . . 8 (((φ → (x = v y = u)) ([z / x][w / y]φ → (z = v w = u))) → ((φ [z / x][w / y]φ) → ((x = v y = u) (z = v w = u))))
37 equtr2 1688 . . . . . . . . . 10 ((x = v z = v) → x = z)
38 equtr2 1688 . . . . . . . . . 10 ((y = u w = u) → y = w)
3937, 38anim12i 549 . . . . . . . . 9 (((x = v z = v) (y = u w = u)) → (x = z y = w))
4039an4s 799 . . . . . . . 8 (((x = v y = u) (z = v w = u)) → (x = z y = w))
4136, 40syl6 29 . . . . . . 7 (((φ → (x = v y = u)) ([z / x][w / y]φ → (z = v w = u))) → ((φ [z / x][w / y]φ) → (x = z y = w)))
42412alimi 1560 . . . . . 6 (zw((φ → (x = v y = u)) ([z / x][w / y]φ → (z = v w = u))) → zw((φ [z / x][w / y]φ) → (x = z y = w)))
43422alimi 1560 . . . . 5 (xyzw((φ → (x = v y = u)) ([z / x][w / y]φ → (z = v w = u))) → xyzw((φ [z / x][w / y]φ) → (x = z y = w)))
4435, 43syl 15 . . . 4 (xy(φ → (x = v y = u)) → xyzw((φ [z / x][w / y]φ) → (x = z y = w)))
4544exlimivv 1635 . . 3 (vuxy(φ → (x = v y = u)) → xyzw((φ [z / x][w / y]φ) → (x = z y = w)))
466, 45sylbir 204 . 2 (zwxy(φ → (x = z y = w)) → xyzw((φ [z / x][w / y]φ) → (x = z y = w)))
47 alrot4 1739 . . . . 5 (xyzw((φ [z / x][w / y]φ) → (x = z y = w)) ↔ zwxy((φ [z / x][w / y]φ) → (x = z y = w)))
48 pm3.21 435 . . . . . . . . . . . 12 ([z / x][w / y]φ → (φ → (φ [z / x][w / y]φ)))
4948imim1d 69 . . . . . . . . . . 11 ([z / x][w / y]φ → (((φ [z / x][w / y]φ) → (x = z y = w)) → (φ → (x = z y = w))))
5013, 49alimd 1764 . . . . . . . . . 10 ([z / x][w / y]φ → (y((φ [z / x][w / y]φ) → (x = z y = w)) → y(φ → (x = z y = w))))
519, 50alimd 1764 . . . . . . . . 9 ([z / x][w / y]φ → (xy((φ [z / x][w / y]φ) → (x = z y = w)) → xy(φ → (x = z y = w))))
5251com12 27 . . . . . . . 8 (xy((φ [z / x][w / y]φ) → (x = z y = w)) → ([z / x][w / y]φxy(φ → (x = z y = w))))
5352alimi 1559 . . . . . . 7 (wxy((φ [z / x][w / y]φ) → (x = z y = w)) → w([z / x][w / y]φxy(φ → (x = z y = w))))
54 exim 1575 . . . . . . 7 (w([z / x][w / y]φxy(φ → (x = z y = w))) → (w[z / x][w / y]φwxy(φ → (x = z y = w))))
5553, 54syl 15 . . . . . 6 (wxy((φ [z / x][w / y]φ) → (x = z y = w)) → (w[z / x][w / y]φwxy(φ → (x = z y = w))))
5655alimi 1559 . . . . 5 (zwxy((φ [z / x][w / y]φ) → (x = z y = w)) → z(w[z / x][w / y]φwxy(φ → (x = z y = w))))
5747, 56sylbi 187 . . . 4 (xyzw((φ [z / x][w / y]φ) → (x = z y = w)) → z(w[z / x][w / y]φwxy(φ → (x = z y = w))))
58 exim 1575 . . . 4 (z(w[z / x][w / y]φwxy(φ → (x = z y = w))) → (zw[z / x][w / y]φzwxy(φ → (x = z y = w))))
5957, 58syl 15 . . 3 (xyzw((φ [z / x][w / y]φ) → (x = z y = w)) → (zw[z / x][w / y]φzwxy(φ → (x = z y = w))))
60 alnex 1543 . . . . . 6 (w ¬ [z / x][w / y]φ ↔ ¬ w[z / x][w / y]φ)
6160albii 1566 . . . . 5 (zw ¬ [z / x][w / y]φz ¬ w[z / x][w / y]φ)
62 alnex 1543 . . . . 5 (z ¬ w[z / x][w / y]φ ↔ ¬ zw[z / x][w / y]φ)
6361, 62bitri 240 . . . 4 (zw ¬ [z / x][w / y]φ ↔ ¬ zw[z / x][w / y]φ)
64 nfv 1619 . . . . . . 7 z ¬ φ
65 nfv 1619 . . . . . . 7 w ¬ φ
669nfn 1793 . . . . . . 7 x ¬ [z / x][w / y]φ
6713nfn 1793 . . . . . . 7 y ¬ [z / x][w / y]φ
6818notbid 285 . . . . . . 7 ((x = z y = w) → (¬ φ ↔ ¬ [z / x][w / y]φ))
6964, 65, 66, 67, 68cbval2 2004 . . . . . 6 (xy ¬ φzw ¬ [z / x][w / y]φ)
70 pm2.21 100 . . . . . . 7 φ → (φ → (x = z y = w)))
71702alimi 1560 . . . . . 6 (xy ¬ φxy(φ → (x = z y = w)))
7269, 71sylbir 204 . . . . 5 (zw ¬ [z / x][w / y]φxy(φ → (x = z y = w)))
73 19.8a 1756 . . . . . 6 (wxy(φ → (x = z y = w)) → zwxy(φ → (x = z y = w)))
747319.23bi 1759 . . . . 5 (xy(φ → (x = z y = w)) → zwxy(φ → (x = z y = w)))
7572, 74syl 15 . . . 4 (zw ¬ [z / x][w / y]φzwxy(φ → (x = z y = w)))
7663, 75sylbir 204 . . 3 zw[z / x][w / y]φzwxy(φ → (x = z y = w)))
7759, 76pm2.61d1 151 . 2 (xyzw((φ [z / x][w / y]φ) → (x = z y = w)) → zwxy(φ → (x = z y = w)))
7846, 77impbii 180 1 (zwxy(φ → (x = z y = w)) ↔ xyzw((φ [z / x][w / y]φ) → (x = z y = w)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 176   ∧ wa 358  ∀wal 1540  ∃wex 1541   = wceq 1642  [wsb 1648 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 This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649 This theorem is referenced by:  2mos  2283  2eu6  2289
 Copyright terms: Public domain W3C validator