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

Theorem vtoclbg 3258
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 335 . 2 (𝑥 = 𝐴 → ((𝜑𝜓) ↔ (𝜒𝜃)))
4 vtoclbg.3 . 2 (𝜑𝜓)
53, 4vtoclg 3257 1 (𝐴𝑉 → (𝜒𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1480  wcel 1992
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-9 2001  ax-12 2049  ax-ext 2606
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-clab 2613  df-cleq 2619  df-clel 2622  df-v 3193
This theorem is referenced by:  alexeqg  3320  pm13.183  3332  sbc8g  3430  sbc2or  3431  sbcco  3445  sbc5  3447  sbcie2g  3456  eqsbc3  3462  sbcng  3463  sbcimg  3464  sbcan  3465  sbcor  3466  sbcbig  3467  sbcal  3472  sbcex2  3473  sbcel1v  3482  sbcreu  3502  csbiebg  3542  sbcel12  3960  sbceqg  3961  elpwg  4143  snssg  4301  preq12bg  4359  elintgOLD  4454  elintrabg  4459  sbcbr123  4671  opelresg  5367  inisegn0  5460  funfvima3  6450  elixpsn  7892  ixpsnf1o  7893  domeng  7914  1sdom  8108  rankcf  9544  eldm3  31352  br1steqg  31368  br2ndeqg  31369  elima4  31373  brsset  31630  brbigcup  31639  elfix2  31645  elfunsg  31657  elsingles  31659  funpartlem  31683  ellines  31893  elhf2g  31917  cover2g  33127  sbcrexgOLD  36815  sbcangOLD  38207  sbcorgOLD  38208  sbcalgOLD  38220  sbcexgOLD  38221  sbcel12gOLD  38222  sbcel1gvOLD  38563
  Copyright terms: Public domain W3C validator