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

Theorem vtoclgf 3555
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 3493 . 2 (𝐴𝑉𝐴 ∈ V)
2 vtoclgf.1 . . . 4 𝑥𝐴
32issetf 3489 . . 3 (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
4 vtoclgf.2 . . . 4 𝑥𝜓
5 vtoclgf.4 . . . . 5 𝜑
6 vtoclgf.3 . . . . 5 (𝑥 = 𝐴 → (𝜑𝜓))
75, 6mpbii 232 . . . 4 (𝑥 = 𝐴𝜓)
84, 7exlimi 2211 . . 3 (∃𝑥 𝑥 = 𝐴𝜓)
93, 8sylbi 216 . 2 (𝐴 ∈ V → 𝜓)
101, 9syl 17 1 (𝐴𝑉𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205   = wceq 1542  wex 1782  wnf 1786  wcel 2107  wnfc 2884  Vcvv 3475
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-v 3477
This theorem is referenced by:  vtocl2gf  3561  vtocl3gf  3562  vtoclgaf  3565  elabgf  3665  fsumsplit1  15691  ssiun2sf  31791  subtr  35199  subtr2  35200  supxrgere  44043  supxrgelem  44047  supxrge  44048  fmuldfeqlem1  44298  fprodcnlem  44315  climsuse  44324  dvnmptdivc  44654  dvmptfprodlem  44660  stoweidlem59  44775  fourierdlem31  44854  sge0f1o  45098  sge0fodjrnlem  45132
  Copyright terms: Public domain W3C validator