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

Theorem vtoclbg 3566
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 347 . 2 (𝑥 = 𝐴 → ((𝜑𝜓) ↔ (𝜒𝜃)))
4 vtoclbg.3 . 2 (𝜑𝜓)
53, 4vtoclg 3565 1 (𝐴𝑉 → (𝜒𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207   = wceq 1528  wcel 2105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-nf 1776  df-cleq 2811  df-clel 2890
This theorem is referenced by:  alexeqg  3641  pm13.183  3656  pm13.183OLD  3657  sbc8g  3777  sbc2or  3778  sbccow  3792  sbcco  3795  sbc5  3797  sbcie2g  3808  eqsbc3  3814  eqsbc3OLD  3815  sbcng  3816  sbcimg  3817  sbcan  3818  sbcor  3819  sbcbig  3820  sbcal  3830  sbcex2  3831  sbcel1v  3836  sbcel1vOLD  3837  sbcreu  3856  csbiebg  3912  sbcel12  4357  sbceqg  4358  elpwgOLD  4545  preq12bg  4776  elintrabg  4880  sbcbr123  5111  inisegn0  5954  fsn2g  6892  funfvima3  6989  elixpsn  8489  ixpsnf1o  8490  domeng  8511  1sdom  8709  rankcf  10187  eldm3  32894  elima4  32916  brsset  33247  brbigcup  33256  elfix2  33262  elfunsg  33274  elsingles  33276  funpartlem  33300  ellines  33510  elhf2g  33534  cover2g  34871  sbcrexgOLD  39260
  Copyright terms: Public domain W3C validator