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

Theorem vtoclgf 3236
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 3184 . 2 (𝐴𝑉𝐴 ∈ V)
2 vtoclgf.1 . . . 4 𝑥𝐴
32issetf 3180 . . 3 (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
4 vtoclgf.2 . . . 4 𝑥𝜓
5 vtoclgf.4 . . . . 5 𝜑
6 vtoclgf.3 . . . . 5 (𝑥 = 𝐴 → (𝜑𝜓))
75, 6mpbii 221 . . . 4 (𝑥 = 𝐴𝜓)
84, 7exlimi 2072 . . 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 1976  wnfc 2737  Vcvv 3172
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-v 3174
This theorem is referenced by:  vtocl2gf  3240  vtocl3gf  3241  vtoclgaf  3243  elabgf  3316  fprodsplit1f  14506  ssiun2sf  28566  subtr  31284  subtr2  31285  dmrelrnrel  38210  supxrgere  38287  supxrgelem  38291  supxrge  38292  fsumsplit1  38436  fmuldfeqlem1  38446  fprodcnlem  38463  climsuse  38472  dvnmptdivc  38625  dvmptfprodlem  38631  stoweidlem59  38749  fourierdlem31  38828  sge0f1o  39072  sge0fodjrnlem  39106  salpreimagelt  39392  salpreimalegt  39394
  Copyright terms: Public domain W3C validator