New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  vtoclbg GIF version

Theorem vtoclbg 2915
 Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 29-Apr-1994.)
Hypotheses
Ref Expression
vtoclbg.1 (x = A → (φχ))
vtoclbg.2 (x = A → (ψθ))
vtoclbg.3 (φψ)
Assertion
Ref Expression
vtoclbg (A V → (χθ))
Distinct variable groups:   x,A   χ,x   θ,x
Allowed substitution hints:   φ(x)   ψ(x)   V(x)

Proof of Theorem vtoclbg
StepHypRef Expression
1 vtoclbg.1 . . 3 (x = A → (φχ))
2 vtoclbg.2 . . 3 (x = A → (ψθ))
31, 2bibi12d 312 . 2 (x = A → ((φψ) ↔ (χθ)))
4 vtoclbg.3 . 2 (φψ)
53, 4vtoclg 2914 1 (A V → (χθ))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 176   = wceq 1642   ∈ wcel 1710 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-v 2861 This theorem is referenced by:  pm13.183  2979  sbc8g  3053  sbc2or  3054  sbcco  3068  sbc5  3070  sbcie2g  3079  eqsbc3  3085  sbcng  3086  sbcimg  3087  sbcan  3088  sbcang  3089  sbcor  3090  sbcorg  3091  sbcbig  3092  sbcal  3093  sbcalg  3094  sbcex2  3095  sbcexg  3096  sbc3ang  3104  sbcel1gv  3105  sbcel2gv  3106  sbcralg  3120  sbcrexg  3121  sbcreug  3122  sbcel12g  3151  sbceqg  3152  csbiebg  3175  elpwg  3729  snssg  3844  elintg  3934  elintrabg  3939  preq12bg  4128  sbcbrg  4685  opbr1st  5501  opbr2nd  5502  elfix  5787  otelins2  5791  otelins3  5792  elfunsg  5830  brfns  5833
 Copyright terms: Public domain W3C validator