ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  vtoclbg GIF version

Theorem vtoclbg 2748
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 234 . 2 (𝑥 = 𝐴 → ((𝜑𝜓) ↔ (𝜒𝜃)))
4 vtoclbg.3 . 2 (𝜑𝜓)
53, 4vtoclg 2747 1 (𝐴𝑉 → (𝜒𝜃))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104   = wceq 1332  wcel 1481
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122
This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-v 2689
This theorem is referenced by:  pm13.183  2823  sbc8g  2917  sbcco  2931  sbc5  2933  sbcie2g  2943  eqsbc3  2949  sbcng  2950  sbcimg  2951  sbcan  2952  sbcang  2953  sbcor  2954  sbcorg  2955  sbcbig  2956  sbcal  2961  sbcalg  2962  sbcex2  2963  sbcexg  2964  sbcel1v  2972  sbcralg  2988  sbcreug  2990  sbcel12g  3018  sbceqg  3019  csbiebg  3043  elpwg  3519  snssg  3660  preq12bg  3704  elintg  3783  elintrabg  3788  sbcbrg  3986  opelresg  4830  elixpsn  6633  ixpsnf1o  6634  domeng  6650
  Copyright terms: Public domain W3C validator