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

Theorem vtoclgaf 3564
Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 17-Feb-2006.) (Revised by Mario Carneiro, 10-Oct-2016.)
Hypotheses
Ref Expression
vtoclgaf.1 𝑥𝐴
vtoclgaf.2 𝑥𝜓
vtoclgaf.3 (𝑥 = 𝐴 → (𝜑𝜓))
vtoclgaf.4 (𝑥𝐵𝜑)
Assertion
Ref Expression
vtoclgaf (𝐴𝐵𝜓)
Distinct variable group:   𝑥,𝐵
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥)   𝐴(𝑥)

Proof of Theorem vtoclgaf
StepHypRef Expression
1 vtoclgaf.1 . . 3 𝑥𝐴
21nfel1 2919 . . . 4 𝑥 𝐴𝐵
3 vtoclgaf.2 . . . 4 𝑥𝜓
42, 3nfim 1899 . . 3 𝑥(𝐴𝐵𝜓)
5 eleq1 2821 . . . 4 (𝑥 = 𝐴 → (𝑥𝐵𝐴𝐵))
6 vtoclgaf.3 . . . 4 (𝑥 = 𝐴 → (𝜑𝜓))
75, 6imbi12d 344 . . 3 (𝑥 = 𝐴 → ((𝑥𝐵𝜑) ↔ (𝐴𝐵𝜓)))
8 vtoclgaf.4 . . 3 (𝑥𝐵𝜑)
91, 4, 7, 8vtoclgf 3554 . 2 (𝐴𝐵 → (𝐴𝐵𝜓))
109pm2.43i 52 1 (𝐴𝐵𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205   = wceq 1541  wnf 1785  wcel 2106  wnfc 2883
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-v 3476
This theorem is referenced by:  ssiun2s  5051  iunopeqop  5521  fvmptss  7010  fvmptf  7019  fmptco  7126  tfis  7843  inar1  10769  sumss  15669  fprodn0  15922  prmind2  16621  lss1d  20573  itg2splitlem  25265  dgrle  25756  cnlnadjlem5  31319  poimirlem25  36508  stoweidlem26  44732
  Copyright terms: Public domain W3C validator