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

Theorem vtoclgf 3141
 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 3089 . 2 (𝐴𝑉𝐴 ∈ V)
2 vtoclgf.1 . . . 4 𝑥𝐴
32issetf 3085 . . 3 (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
4 vtoclgf.2 . . . 4 𝑥𝜓
5 vtoclgf.4 . . . . 5 𝜑
6 vtoclgf.3 . . . . 5 (𝑥 = 𝐴 → (𝜑𝜓))
75, 6mpbii 221 . . . 4 (𝑥 = 𝐴𝜓)
84, 7exlimi 2043 . . 3 (∃𝑥 𝑥 = 𝐴𝜓)
93, 8sylbi 205 . 2 (𝐴 ∈ V → 𝜓)
101, 9syl 17 1 (𝐴𝑉𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 194   = wceq 1474  ∃wex 1694  Ⅎwnf 1698   ∈ wcel 1938  Ⅎwnfc 2642  Vcvv 3077 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494 This theorem depends on definitions:  df-bi 195  df-an 384  df-tru 1477  df-ex 1695  df-nf 1699  df-sb 1831  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-v 3079 This theorem is referenced by:  vtocl2gf  3145  vtocl3gf  3146  vtoclgaf  3148  elabgf  3221  fprodsplit1f  14427  ssiun2sf  28549  subtr  31314  subtr2  31315  dmrelrnrel  38298  supxrgere  38376  supxrgelem  38380  supxrge  38381  fsumsplit1  38525  fmuldfeqlem1  38535  fprodcnlem  38552  climsuse  38561  dvnmptdivc  38718  dvmptfprodlem  38724  stoweidlem59  38842  fourierdlem31  38921  fourierdlem31OLD  38922  sge0f1o  39169  sge0fodjrnlem  39203  salpreimagelt  39489  salpreimalegt  39491
 Copyright terms: Public domain W3C validator