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

Theorem vtoclbg 3423
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 3422 1 (𝐴𝑉 → (𝜒𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197   = wceq 1634  wcel 2148
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1873  ax-4 1888  ax-5 1994  ax-6 2060  ax-7 2096  ax-9 2157  ax-12 2206  ax-ext 2754
This theorem depends on definitions:  df-bi 198  df-an 384  df-or 864  df-tru 1637  df-ex 1856  df-nf 1861  df-sb 2053  df-clab 2761  df-cleq 2767  df-clel 2770  df-v 3357
This theorem is referenced by:  alexeqg  3488  pm13.183  3501  sbc8g  3601  sbc2or  3602  sbcco  3616  sbc5  3618  sbcie2g  3627  eqsbc3  3633  sbcng  3634  sbcimg  3635  sbcan  3636  sbcor  3637  sbcbig  3638  sbcal  3643  sbcex2  3644  sbcel1v  3652  sbcreu  3670  csbiebg  3711  sbcel12  4137  sbceqg  4138  elpwg  4315  snssgOLD  4463  preq12bg  4528  elintrabg  4635  sbcbr123  4851  opelresgOLD  5558  inisegn0  5648  funfvima3  6658  elixpsn  8122  ixpsnf1o  8123  domeng  8144  1sdom  8340  rankcf  9822  eldm3  32006  br1steqgOLD  32027  br2ndeqgOLD  32028  elima4  32032  brsset  32350  brbigcup  32359  elfix2  32365  elfunsg  32377  elsingles  32379  funpartlem  32403  ellines  32613  elhf2g  32637  cover2g  33858  sbcrexgOLD  37890  sbcangOLD  39277  sbcorgOLD  39278  sbcalgOLD  39290  sbcexgOLD  39291  sbcel12gOLD  39292  sbcel1gvOLD  39628
  Copyright terms: Public domain W3C validator