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

Theorem vtoclgaf 3244
 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 2765 . . . 4 𝑥 𝐴𝐵
3 vtoclgaf.2 . . . 4 𝑥𝜓
42, 3nfim 1813 . . 3 𝑥(𝐴𝐵𝜓)
5 eleq1 2676 . . . 4 (𝑥 = 𝐴 → (𝑥𝐵𝐴𝐵))
6 vtoclgaf.3 . . . 4 (𝑥 = 𝐴 → (𝜑𝜓))
75, 6imbi12d 333 . . 3 (𝑥 = 𝐴 → ((𝑥𝐵𝜑) ↔ (𝐴𝐵𝜓)))
8 vtoclgaf.4 . . 3 (𝑥𝐵𝜑)
91, 4, 7, 8vtoclgf 3237 . 2 (𝐴𝐵 → (𝐴𝐵𝜓))
109pm2.43i 50 1 (𝐴𝐵𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   = wceq 1475  Ⅎwnf 1699   ∈ wcel 1977  Ⅎwnfc 2738 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175 This theorem is referenced by:  vtoclga  3245  ssiun2s  4500  iunopeqop  4906  fvmptss  6201  fvmptf  6209  fmptco  6303  tfis  6946  inar1  9476  sumss  14302  fprodn0  14548  prmind2  15236  lss1d  18784  itg2splitlem  23321  dgrle  23803  cnlnadjlem5  28314  poimirlem25  32604  stoweidlem26  38919
 Copyright terms: Public domain W3C validator