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

Theorem vtoclbg 3399
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 334 . 2 (𝑥 = 𝐴 → ((𝜑𝜓) ↔ (𝜒𝜃)))
4 vtoclbg.3 . 2 (𝜑𝜓)
53, 4vtoclg 3398 1 (𝐴𝑉 → (𝜒𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1624  wcel 2131
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-12 2188  ax-ext 2732
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-clab 2739  df-cleq 2745  df-clel 2748  df-v 3334
This theorem is referenced by:  alexeqg  3463  pm13.183  3476  sbc8g  3576  sbc2or  3577  sbcco  3591  sbc5  3593  sbcie2g  3602  eqsbc3  3608  sbcng  3609  sbcimg  3610  sbcan  3611  sbcor  3612  sbcbig  3613  sbcal  3618  sbcex2  3619  sbcel1v  3628  sbcreu  3648  csbiebg  3689  sbcel12  4118  sbceqg  4119  elpwg  4302  snssgOLD  4453  preq12bg  4522  elintgOLD  4628  elintrabg  4633  sbcbr123  4850  opelresgOLD  5555  inisegn0  5647  funfvima3  6650  elixpsn  8105  ixpsnf1o  8106  domeng  8127  1sdom  8320  rankcf  9783  eldm3  31950  br1steqgOLD  31971  br2ndeqgOLD  31972  elima4  31976  brsset  32294  brbigcup  32303  elfix2  32309  elfunsg  32321  elsingles  32323  funpartlem  32347  ellines  32557  elhf2g  32581  cover2g  33814  sbcrexgOLD  37843  sbcangOLD  39233  sbcorgOLD  39234  sbcalgOLD  39246  sbcexgOLD  39247  sbcel12gOLD  39248  sbcel1gvOLD  39585
  Copyright terms: Public domain W3C validator