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

Theorem vtoclbg 3526
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 348 . 2 (𝑥 = 𝐴 → ((𝜑𝜓) ↔ (𝜒𝜃)))
4 vtoclbg.3 . 2 (𝜑𝜓)
53, 4vtoclg 3524 1 (𝐴𝑉 → (𝜒𝜃))
Colors of variables:    wff setvar class
This proof depends on syntax axioms:  wi 4  wb 209   = wceq 1570  wcel 2146
This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148
This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-clel 2840
This theorem is used by:  alexeqg  3612  pm13.183  3627  elab6g  3630  elabgw  3638  sbc8g  3754  sbc2or  3755  sbccow  3769  sbcco  3772  sbc5ALT  3775  sbcie2g  3786  eqsbc1  3792  sbcng  3793  sbcimg  3794  sbcan  3795  sbcor  3796  sbcbig  3797  sbcal  3805  sbcex2  3806  sbcel1v  3811  sbcreu  3830  csbiebg  3886  sbcel12  4376  sbceqg  4377  csbie2df  4408  preq12bg  4820  elintrabg  4928  sbcbr123  5167  inisegn0  6102  fsn2g  7138  funfvima3  7241  elixpsn  8941  ixpsnf1o  8942  domeng  8965  rankcf  10779  kardeng  35629  eldm3  36292  elima4  36307  brsset  36418  brbigcup  36427  elfix2  36433  elfunsg  36445  elsingles  36447  funpartlem  36473  ellines  36683  elhf2g  36707  bj-elpwgALT  37749  cover2g  38427
  Copyright terms: Public domain W3C validator