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

Theorem vtoclgf 3126
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 3075 . 2 (𝐴𝑉𝐴 ∈ V)
2 vtoclgf.1 . . . 4 𝑥𝐴
32issetf 3071 . . 3 (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
4 vtoclgf.2 . . . 4 𝑥𝜓
5 vtoclgf.4 . . . . 5 𝜑
6 vtoclgf.3 . . . . 5 (𝑥 = 𝐴 → (𝜑𝜓))
75, 6mpbii 218 . . . 4 (𝑥 = 𝐴𝜓)
84, 7exlimi 2048 . . 3 (∃𝑥 𝑥 = 𝐴𝜓)
93, 8sylbi 202 . 2 (𝐴 ∈ V → 𝜓)
101, 9syl 17 1 (𝐴𝑉𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 191   = wceq 1468  wex 1692  wnf 1696  wcel 1937  wnfc 2633  Vcvv 3066
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1698  ax-4 1711  ax-5 1789  ax-6 1836  ax-7 1883  ax-10 1965  ax-11 1970  ax-12 1983  ax-13 2137  ax-ext 2485
This theorem depends on definitions:  df-bi 192  df-an 380  df-tru 1471  df-ex 1693  df-nf 1697  df-sb 1829  df-clab 2492  df-cleq 2498  df-clel 2501  df-nfc 2635  df-v 3068
This theorem is referenced by:  vtocl2gf  3130  vtocl3gf  3131  vtoclgaf  3133  elabgf  3206  fprodsplit1f  14204  ssiun2sf  28334  subtr  31119  subtr2  31120  supxrgere  37932  supxrgelem  37936  supxrge  37937  fsumsplit1  38052  fmuldfeqlem1  38062  fprodcnlem  38081  climsuse  38091  dvnmptdivc  38232  dvmptfprodlem  38238  stoweidlem59  38356  fourierdlem31  38436  fourierdlem31OLD  38437  sge0f1o  38670  sge0fodjrnlem  38704
  Copyright terms: Public domain W3C validator