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

Theorem vtocl3 2911
 Description: Implicit substitution of classes for setvar variables. (Contributed by NM, 3-Jun-1995.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)
Hypotheses
Ref Expression
vtocl3.1 A V
vtocl3.2 B V
vtocl3.3 C V
vtocl3.4 ((x = A y = B z = C) → (φψ))
vtocl3.5 φ
Assertion
Ref Expression
vtocl3 ψ
Distinct variable groups:   x,y,z,A   x,B,y,z   x,C,y,z   ψ,x,y,z
Allowed substitution hints:   φ(x,y,z)

Proof of Theorem vtocl3
StepHypRef Expression
1 vtocl3.1 . . . . . . 7 A V
21isseti 2865 . . . . . 6 x x = A
3 vtocl3.2 . . . . . . 7 B V
43isseti 2865 . . . . . 6 y y = B
5 vtocl3.3 . . . . . . 7 C V
65isseti 2865 . . . . . 6 z z = C
7 eeeanv 1914 . . . . . . 7 (xyz(x = A y = B z = C) ↔ (x x = A y y = B z z = C))
8 vtocl3.4 . . . . . . . . . 10 ((x = A y = B z = C) → (φψ))
98biimpd 198 . . . . . . . . 9 ((x = A y = B z = C) → (φψ))
109eximi 1576 . . . . . . . 8 (z(x = A y = B z = C) → z(φψ))
11102eximi 1577 . . . . . . 7 (xyz(x = A y = B z = C) → xyz(φψ))
127, 11sylbir 204 . . . . . 6 ((x x = A y y = B z z = C) → xyz(φψ))
132, 4, 6, 12mp3an 1277 . . . . 5 xyz(φψ)
14 19.36v 1896 . . . . . 6 (z(φψ) ↔ (zφψ))
15142exbii 1583 . . . . 5 (xyz(φψ) ↔ xy(zφψ))
1613, 15mpbi 199 . . . 4 xy(zφψ)
17 19.36v 1896 . . . . 5 (y(zφψ) ↔ (yzφψ))
1817exbii 1582 . . . 4 (xy(zφψ) ↔ x(yzφψ))
1916, 18mpbi 199 . . 3 x(yzφψ)
201919.36aiv 1897 . 2 (xyzφψ)
21 vtocl3.5 . . 3 φ
2221gen2 1547 . 2 yzφ
2320, 22mpg 1548 1 ψ
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 176   ∧ w3a 934  ∀wal 1540  ∃wex 1541   = wceq 1642   ∈ wcel 1710  Vcvv 2859 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-ext 2334 This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-v 2861 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator