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

Theorem vtoclbg 3460
Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 29-Apr-1994.)
Hypotheses
Ref Expression
vtoclbg.1 (𝑥 = 𝐴 → (𝜑𝜒))
vtoclbg.2 (𝑥 = 𝐴 → (𝜓𝜃))
vtoclbg.3 (𝜑𝜓)
Assertion
Ref Expression
vtoclbg (𝐴𝑉 → (𝜒𝜃))
Distinct variable groups:   𝑥,𝐴   𝜒,𝑥   𝜃,𝑥
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥)   𝑉(𝑥)

Proof of Theorem vtoclbg
StepHypRef Expression
1 vtoclbg.1 . . 3 (𝑥 = 𝐴 → (𝜑𝜒))
2 vtoclbg.2 . . 3 (𝑥 = 𝐴 → (𝜓𝜃))
31, 2bibi12d 336 . 2 (𝑥 = 𝐴 → ((𝜑𝜓) ↔ (𝜒𝜃)))
4 vtoclbg.3 . 2 (𝜑𝜓)
53, 4vtoclg 3459 1 (𝐴𝑉 → (𝜒𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197   = wceq 1637  wcel 2156
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-12 2214  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-v 3393
This theorem is referenced by:  alexeqg  3526  pm13.183  3539  sbc8g  3641  sbc2or  3642  sbcco  3656  sbc5  3658  sbcie2g  3667  eqsbc3  3673  sbcng  3674  sbcimg  3675  sbcan  3676  sbcor  3677  sbcbig  3678  sbcal  3683  sbcex2  3684  sbcel1v  3692  sbcreu  3710  csbiebg  3751  sbcel12  4180  sbceqg  4181  elpwg  4359  snssgOLD  4507  preq12bg  4573  elintrabg  4682  sbcbr123  4898  opelresgOLD  5609  inisegn0  5707  funfvima3  6720  elixpsn  8184  ixpsnf1o  8185  domeng  8206  1sdom  8402  rankcf  9884  eldm3  31973  br1steqgOLD  31994  br2ndeqgOLD  31995  elima4  31999  brsset  32317  brbigcup  32326  elfix2  32332  elfunsg  32344  elsingles  32346  funpartlem  32370  ellines  32580  elhf2g  32604  cover2g  33821  sbcrexgOLD  37851  sbcangOLD  39237  sbcorgOLD  39238  sbcalgOLD  39250  sbcexgOLD  39251  sbcel12gOLD  39252  sbcel1gvOLD  39588
  Copyright terms: Public domain W3C validator