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

Theorem vtoclbg 3574
 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 3573 1 (𝐴𝑉 → (𝜒𝜃))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 207   = wceq 1530   ∈ wcel 2107 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-12 2169  ax-ext 2798 This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1774  df-nf 1778  df-cleq 2819  df-clel 2898 This theorem is referenced by:  alexeqg  3648  pm13.183  3663  pm13.183OLD  3664  sbc8g  3784  sbc2or  3785  sbccow  3799  sbcco  3802  sbc5  3804  sbcie2g  3815  eqsbc3  3821  eqsbc3OLD  3822  sbcng  3823  sbcimg  3824  sbcan  3825  sbcor  3826  sbcbig  3827  sbcal  3837  sbcex2  3838  sbcel1v  3843  sbcel1vOLD  3844  sbcreu  3863  csbiebg  3919  sbcel12  4364  sbceqg  4365  elpwgOLD  4552  preq12bg  4783  elintrabg  4887  sbcbr123  5117  inisegn0  5959  fsn2g  6896  funfvima3  6992  elixpsn  8490  ixpsnf1o  8491  domeng  8512  1sdom  8710  rankcf  10188  eldm3  32881  elima4  32903  brsset  33234  brbigcup  33243  elfix2  33249  elfunsg  33261  elsingles  33263  funpartlem  33287  ellines  33497  elhf2g  33521  cover2g  34858  sbcrexgOLD  39247
 Copyright terms: Public domain W3C validator