MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  vtoclgf Structured version   Visualization version   GIF version

Theorem vtoclgf 3392
Description: Implicit substitution of a class for a setvar variable, with bound-variable hypotheses in place of disjoint variable restrictions. (Contributed by NM, 21-Sep-2003.) (Proof shortened by Mario Carneiro, 10-Oct-2016.)
Hypotheses
Ref Expression
vtoclgf.1 𝑥𝐴
vtoclgf.2 𝑥𝜓
vtoclgf.3 (𝑥 = 𝐴 → (𝜑𝜓))
vtoclgf.4 𝜑
Assertion
Ref Expression
vtoclgf (𝐴𝑉𝜓)

Proof of Theorem vtoclgf
StepHypRef Expression
1 elex 3340 . 2 (𝐴𝑉𝐴 ∈ V)
2 vtoclgf.1 . . . 4 𝑥𝐴
32issetf 3336 . . 3 (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
4 vtoclgf.2 . . . 4 𝑥𝜓
5 vtoclgf.4 . . . . 5 𝜑
6 vtoclgf.3 . . . . 5 (𝑥 = 𝐴 → (𝜑𝜓))
75, 6mpbii 223 . . . 4 (𝑥 = 𝐴𝜓)
84, 7exlimi 2221 . . 3 (∃𝑥 𝑥 = 𝐴𝜓)
93, 8sylbi 207 . 2 (𝐴 ∈ V → 𝜓)
101, 9syl 17 1 (𝐴𝑉𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1620  wex 1841  wnf 1845  wcel 2127  wnfc 2877  Vcvv 3328
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-clab 2735  df-cleq 2741  df-clel 2744  df-nfc 2879  df-v 3330
This theorem is referenced by:  vtocl2gf  3396  vtocl3gf  3397  vtoclgaf  3399  elabgf  3476  fprodsplit1f  14891  ssiun2sf  29656  subtr  32585  subtr2  32586  supxrgere  40016  supxrgelem  40020  supxrge  40021  fsumsplit1  40276  fmuldfeqlem1  40286  fprodcnlem  40303  climsuse  40312  dvnmptdivc  40625  dvmptfprodlem  40631  stoweidlem59  40748  fourierdlem31  40827  sge0f1o  41071  sge0fodjrnlem  41105  salpreimagelt  41393  salpreimalegt  41395
  Copyright terms: Public domain W3C validator